Proof of Predicative Formulas for Bijections from a Segment [n] and for Increasing Listings

Auxiliary formulas. Let $\mathrm{seg}(s,n)$ be the formula of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), with the set variables $s$ and $n$ for its $z$ and $n$ and the parameters $\mathbb{N}$ and $\le$ for its class variables $Y$ and $R$; it is predicative, and for every set $s$ and every $n\in\mathbb{N}_{0}$, $\mathrm{seg}(s,n)$ holds if and only if $s=[n]$. Let $\mu$, $\iota$ and $\sigma$ be the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (viii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ix), and let $(i,j)\in{\le}$ and $(u,v)\in{<}$, for the parameters $\le$ of $\mathbb{N}_{0}$ and $<$ of $\mathbb{R}$, and $(i,u)\in x$ and $(j,v)\in x$ be the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii). These formulas are used with the set variables below put for their displayed ones, 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 (i); the letters $i$, $j$, $s$, $u$ and $v$ are set variables distinct from each other, from $f$, $x$, $n$, $B$ and from the parameters.

Let

$$\theta(x,i,j):\quad\forall u\,\bigl((i,u)\in x\Rightarrow\forall v\,((j,v)\in x\Rightarrow(u,v)\in{<})\bigr).$$

By Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i), with $j$, $v$ and $x$ for its $x$, $z$ and $F$ and the predicative formula $(u,v)\in{<}$ for its $\varphi$, the formula $\forall v\,((j,v)\in x\Rightarrow(u,v)\in{<})$ is predicative, and, whenever the value of $x$ is a function, it holds if and only if $(u,x(j))\in{<}$ whenever $j\in\operatorname{dom}x$. Applying Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i) again, with $i$, $u$ and $x$ for its $x$, $z$ and $F$ and this formula for its $\varphi$, $\theta(x,i,j)$ is predicative, and, whenever the value of $x$ is a function, it holds if and only if, for $i\in\operatorname{dom}x$, $(x(i),x(j))\in{<}$ whenever $j\in\operatorname{dom}x$. So, whenever $x$ is a function and $i,j\in\operatorname{dom}x$, $\theta(x,i,j)$ holds if and only if $x(i)<x(j)$.

The formulas. Let

$$\beta(f,n,B):\quad n\in\mathbb{N}_{0}\wedge\exists s\,\bigl(\mathrm{seg}(s,n)\wedge\mu(f,s,B)\wedge\iota(f)\wedge\sigma(f,B)\bigr),$$ $$\lambda(x,n,B):\quad n\in\mathbb{N}_{0}\wedge\exists s\,\Bigl(\mathrm{seg}(s,n)\wedge\mu(x,s,B)\wedge\iota(x)\wedge\sigma(x,B)\wedge\forall i\,\forall j\,\bigl((i\in s\wedge j\in s\wedge(i,j)\in{\le}\wedge\neg\,i=j)\Rightarrow\theta(x,i,j)\bigr)\Bigr).$$

The free variables of $\beta$ are among $f$, $n$, $B$ and the parameters $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$, and those of $\lambda$ among $x$, $n$, $B$ and the parameters $\mathbb{N}_{0}$, $\mathbb{N}$, $\le$ and $<$. The formulas $\mathrm{seg}$, $\mu$, $\iota$, $\sigma$, $\theta$ and the pair memberships are predicative by the results cited above, and $\beta$ and $\lambda$ are built from them, from memberships and from equations by connectives and by quantifiers over set variables only; so no quantifier in them is applied to a class variable, and they are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Proof of (i). Let $f$, $n$ and $B$ be sets. If $n\notin\mathbb{N}_{0}$, both $\beta(f,n,B)$ and the condition fail. Let $n\in\mathbb{N}_{0}$. Then $[n]$ is a set by The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ (i), and $\mathrm{seg}(s,n)$ holds exactly for $s=[n]$; so $\beta(f,n,B)$ holds if and only if $\mu(f,[n],B)\wedge\iota(f)\wedge\sigma(f,B)$ holds, that is, 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), if and only if $f$ is a bijection from $[n]$ onto $B$. So $\beta$ expresses the condition of (i), as in Conditions Expressed by a Predicative Formula, and Guards (ii).

Proof of (ii). Let $x$, $n$ and $B$ be sets. As in the proof of (i), if $n\notin\mathbb{N}_{0}$ both $\lambda(x,n,B)$ and the condition fail; and for $n\in\mathbb{N}_{0}$, $\lambda(x,n,B)$ holds if and only if $x$ is a bijection from $[n]$ onto $B$ and

$$\forall i\,\forall j\,\bigl((i\in[n]\wedge j\in[n]\wedge(i,j)\in{\le}\wedge\neg\,i=j)\Rightarrow\theta(x,i,j)\bigr)$$

holds, 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). Let $x$ be such a bijection. Then $x$ is a map $x:[n]\to B$, so it is a function with $\operatorname{dom}x=[n]$ by Functions, Values of a Function, and Functions from One Class to Another (iii). For $i,j\in[n]$, which lie in $\mathbb{N}_{0}$, $(i,j)\in{\le}\wedge\neg\,i=j$ holds if and only if $i<j$ in $\mathbb{N}_{0}$, by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii), and $\theta(x,i,j)$ holds if and only if $x(i)<x(j)$, by the auxiliary formulas. So the display holds if and only if $x(i)<x(j)$ for all $i,j\in[n]$ with $i<j$. Hence $\lambda(x,n,B)$ holds if and only if the condition of (ii) holds: $\lambda$ expresses it, as in Conditions Expressed by a Predicative Formula, and Guards (ii).