Proof of A Finite Set of Real Numbers Has Exactly One Increasing Listing

For $M\in\mathbb{N}_{0}$ and a subset $B$ of $\mathbb{R}$, call a map $x:[M]\to B$ increasing if $x(i)<x(j)$ for all $i,j\in[M]$ with $i<j$. Here $<$ on $[M]$ is the strict order of $\mathbb{N}_{0}$, and $<$ on $B$ that of $\mathbb{R}$; $\le$ is a partial order on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v), and a total order on $\mathbb{R}$ by The Real Line: Standing Notation and Background for Calculus on Intervals (ii) and Ordered Fields (i).

Let $K$ be the set of those $M\in\mathbb{N}_{0}$ such that, for every subset $B$ of $\mathbb{R}$ and every bijection $f$ from $[M]$ onto $B$, there is exactly one increasing bijection $x:[M]\to B$. (Its defining condition quantifies over sets only, the bijection condition being predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (x), so $K$ is a subset of $\mathbb{N}_{0}$ as in Sets and Maps: Ordinary Notation (iii).) We show $0\in K$ and that $M\in K$ implies $M+1\in K$; as the successor of $M$ is $M+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (v), induction from $0$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (viii)) then gives $N\in K$, and applying this to $B=A$ and a bijection from $[N]$ onto $A$ proves (i).

Base. Let $B\subseteq\mathbb{R}$ and let $f$ be a bijection from $[0]$ onto $B$. As $[0]=\emptyset$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $f$ is increasing, there being no $i\in[0]$. If $y:[0]\to B$ is any increasing bijection, then $\operatorname{dom}y=[0]=\operatorname{dom}f$ by Functions, Values of a Function, and Functions from One Class to Another (iii), and $y(u)=f(u)$ holds for every $u$ in this empty domain; so $y=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). Hence $0\in K$.

Step. Let $M\in K$, let $B\subseteq\mathbb{R}$, and let $f$ be a bijection from $[M+1]$ onto $B$. Then $B$ is finite by Finite Sets (i), and $\#B=M+1$ by The Number of Elements of a Finite Set (i). By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (ii), $[M+1]=[M]\cup\{M+1\}$ and $M+1\notin[M]$; in particular $M+1\in[M+1]$, so $f(M+1)\in B$ and $B\neq\emptyset$. By Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (viii), $B$ has a greatest element $b=\max B$.

Let $B'=B\setminus\{b\}$, a subset of $B$ and of $\mathbb{R}$. Then $B'\cup\{b\}=B$ and $B'\cap\{b\}=\emptyset$; $B'$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv), and $\{b\}$ by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii). By Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (v) and Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products (ii), $M+1=\#B=\#B'+\#\{b\}=\#B'+1$, so $\#B'=M$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv) and Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (v). Hence there is a bijection $f'$ from $[M]$ onto $B'$, by The Number of Elements of a Finite Set (i), and as $M\in K$ there is exactly one increasing bijection $x':[M]\to B'$.

Existence. Since $\operatorname{ran}x'\subseteq B'\subseteq B$, $x'$ is also a map $[M]\to B$ by Functions, Values of a Function, and Functions from One Class to Another (iii). As $M+1\notin[M]$, $b\in B$ and $b\notin B'$, Extending a Map by One Point, and Extending a Bijection by One Point (i) gives a map $h:[M]\cup\{M+1\}\to B$, that is $h:[M+1]\to B$, with $h(i)=x'(i)$ for $i\in[M]$ and $h(M+1)=b$; and by Extending a Map by One Point, and Extending a Bijection by One Point (ii), with $C=B'$, $h$ is a bijection from $[M+1]$ onto $B'\cup\{b\}=B$.

The map $h$ is increasing. Let $i,j\in[M+1]$ with $i<j$; then $i\le M+1$ and $j\le M+1$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i). If $j=M+1$, then $i\neq M+1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iii), so $i\in[M]$; hence $h(i)=x'(i)\in B'$, so $h(i)\in B$ and $h(i)\neq b$, and $h(i)\le b$ as $b$ is the greatest element of $B$; thus $h(i)<b=h(j)$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (ii). Otherwise $j\in[M]$, and $j\neq M+1$, so $j<M+1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (ii); if $i=M+1$, then $M+1<j<M+1$ would give $M+1<M+1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iv), contrary to Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (iii). So $i\in[M]$, and $h(i)=x'(i)<x'(j)=h(j)$ as $x'$ is increasing.

Uniqueness. Let $y:[M+1]\to B$ be an increasing bijection. For $k\in[M]$, $k\in[M]\cup\{M+1\}=[M+1]$, so $k\le M+1$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i) and $k\neq M+1$, so $k<M+1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (ii) and $y(k)<y(M+1)$. Every $u\in B$ is $y(k)$ for some $k\in[M+1]$, as $y$ is surjective, and $k=M+1$ or $k\in[M]$; so $u\le y(M+1)$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (v). Thus $y(M+1)$ is a greatest element of $B$ in the sense of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iii), and $y(M+1)=b$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (i). Consequently $y(k)<b$, so $y(k)\neq b$ and $y(k)\in B'$, for every $k\in[M]$.

The restriction $y|_{[M]}$ is a function with domain $[M]$ and $(y|_{[M]})(k)=y(k)$ for $k\in[M]$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix); its values lie in $B'$, so by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) its range lies in $B'$ and it is a map $y|_{[M]}:[M]\to B'$ by Functions, Values of a Function, and Functions from One Class to Another (iii). It is increasing because $y$ is, and injective because $y$ is. It is surjective onto $B'$: every $u\in B'$ is $y(k)$ for some $k\in[M+1]$, and $k\neq M+1$ as $u\neq b=y(M+1)$, so $k\in[M]$ and $u=(y|_{[M]})(k)$. By Injective, Surjective and Bijective Functions between Classes (iii) it is a bijection, so $y|_{[M]}=x'$ by the uniqueness in $M\in K$, applied to $B'$ and $f'$. Hence $y(i)=x'(i)$ for every $i\in[M]$ and $y(M+1)=b$; as $y$ is a map $[M]\cup\{M+1\}\to B$, the uniqueness in Extending a Map by One Point, and Extending a Bijection by One Point (i) gives $y=h$.

So $M+1\in K$, which completes the induction.