Proof 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

Renaming. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative, $\varphi$ has no part $\exists X\,\psi$ with $X$ a class variable, so every part $\exists s\,\psi$ of $\varphi$ has $s$ a set variable. Both steps defining $\varphi[y/v]$ replace occurrences of set variables by variables, the first only by set variables and the second only at free occurrences, and leave every other symbol in place, so each part of $\varphi$ built by a rule of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula becomes a part built by the same rule, and each part $\exists s\,\psi$ of $\varphi$ becomes a part $\exists t\,\chi$ of $\varphi[y/v]$ with $t$ equal to $s$ or to the set variable $s'$, so $t$ is a set variable. Hence $\varphi[y/v]$ is a formula in which every quantifier is applied to a set variable, so it is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative.

For the second assertion, fix an assignment as there. The value of each $y_{i}$ is a set, by hypothesis if $y_{i}$ is a class variable and by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading if it is a set variable, so it may be assigned to the set variable $v_{i}$. The first step only renames bound variables to set variables occurring nowhere else, so by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading it does not change what the formula says; let $\chi$ be its result. For the second step, prove by induction on the parts of $\chi$, built by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, the following claim for every part $\eta$, every sublist $L$ of the pairs $(v_{1},y_{1}),\dots,(v_{k},y_{k})$ and every assignment: $\eta$ with the free occurrences of the $v_{i}$ in $L$ replaced by the $y_{i}$ holds if and only if $\eta$ holds with each such $v_{i}$ assigned the value of $y_{i}$. An atomic part says the same of the value of $y_{i}$ as it said of $v_{i}$ when $v_{i}$ is assigned that value, and $\neg$ and $\wedge$ commute with the replacement. For a part $\exists s\,\psi$, $s$ is none of $y_{1},\dots,y_{k}$ by the first step, so assigning a set to $s$ leaves the values of all $y_{j}$ unchanged. If $s$ is some $v_{i}$ with $(v_{i},y_{i})$ in $L$, then $v_{i}$ has no free occurrence in $\exists s\,\psi$, so the replacement of $\exists s\,\psi$ is $\exists s$ applied to the replacement of $\psi$ for $L$ with $(v_{i},y_{i})$ removed, and the induction hypothesis for that sublist applies to $\psi$ for each set assigned to $s$; otherwise the induction hypothesis for $L$ applies to $\psi$ for each set assigned to $s$. The case $\eta=\chi$ with the whole list is the second assertion.

Pairs. The expressions $s=(t'_{1},t'_{2})$, $(t'_{1},t'_{2})\in s$ and $((t'_{1},t'_{2}),t'_{3})\in s$ contain no quantifier, and their ordered pairs of set variables are used properly, since the ordered pair of two sets is a set by The Ordered Pair of Two Sets and Nested Tuples §pair. They are therefore predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, that is, the formulas $\pi_{1}$, $\pi_{2}$ and $\pi_{3}$ obtained by eliminating their abbreviations, innermost first, are predicative, and by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols each says, for sets assigned to $t'_{1}$, $t'_{2}$ and $t'_{3}$, what the expression says with the ordered pairs read as those sets. By the clause renaming, $\pi_{j}[t/t']$ is predicative for $j=1,2,3$; and when sets are assigned to the $t_{i}$, it holds if and only if $\pi_{j}$ holds with each $t'_{i}$ assigned the value of $t_{i}$, which is the stated condition on the value of $s$.

Predicativity of the displayed formulas. The formulas $\rho(F)$, $\Phi(F)$, $\mu(F,A,B)$, $\iota(F)$ and $\sigma(F,B)$ and the conjunction in the clause bijective are written with the ordered pair $(u,v)$ of set variables as a defined set symbol, used properly since $(u,v)$ is a set for all sets $u$ and $v$ by The Ordered Pair of Two Sets and Nested Tuples §pair, and every quantifier in them is applied to one of the set variables $p$, $u$, $u'$, $v$, $v'$. They are therefore predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. For a class $F$ and sets $u$ and $v$, the atomic part $(u,v)\in F$ means that the ordered pair of $u$ and $v$ is an element of $F$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §pair-membership.

Below, $F$, $A$ and $B$ are classes, and $p$, $u$, $u'$, $v$ and $v'$ range over sets.

Relation and function. $\rho(F)$ is the condition of Relations, Domain, Range, Inverse and Composition §relation written as a formula, and $\Phi(F)$ is the condition of Functions, Values of a Function, and Functions from One Class to Another §function.

Map. By Functions, Values of a Function, and Functions from One Class to Another §map, $F:A\to B$ means that $F$ is a function, $\operatorname{dom}F=A$ and $\operatorname{ran}F\subseteq B$. As $\operatorname{dom}F=\{u:\exists v\,((u,v)\in F)\}$ by Relations, Domain, Range, Inverse and Composition §domain, Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms gives $A=\operatorname{dom}F$ if and only if $\forall u\,(u\in A\Leftrightarrow\exists v\,((u,v)\in F))$. By Subclasses and Subsets §subclass, $\operatorname{ran}F\subseteq B$ means that every element $v$ of $\operatorname{ran}F$ lies in $B$; as $\operatorname{ran}F=\{v:\exists u\,((u,v)\in F)\}$ by Relations, Domain, Range, Inverse and Composition §range, Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms gives $v\in\operatorname{ran}F$ if and only if $(u,v)\in F$ for some set $u$, so $\operatorname{ran}F\subseteq B$ if and only if $\forall u\,\forall v\,((u,v)\in F\Rightarrow v\in B)$. With the clause function, this gives the clause map.

Injective and surjective. Let $F:A\to B$. By Functions, Values of a Function, and Functions from One Class to Another §map, $F$ is a function with $\operatorname{dom}F=A$, so by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, for all sets $u$ and $v$, $(u,v)\in F$ if and only if $u\in A$ and $v=F(u)$, the value of $F$ at $u$.

Suppose $F$ is injective in the sense of Injective, Surjective and Bijective Functions between Classes §injective, and let $(u,v)\in F$ and $(u',v)\in F$. Then $u,u'\in A$ and $F(u)=v=F(u')$, so $u=u'$; hence $\iota(F)$. Conversely, suppose $\iota(F)$, and let $u,u'\in A$ with $F(u)=F(u')$. With $v=F(u)$, both $(u,v)\in F$ and $(u',v)\in F$, so $u=u'$; hence $F$ is injective.

Suppose $F$ is surjective in the sense of Injective, Surjective and Bijective Functions between Classes §surjective, and let $v\in B$. There is $u\in A$ with $F(u)=v$, so $(u,v)\in F$; hence $\sigma(F,B)$. Conversely, suppose $\sigma(F,B)$, and let $v\in B$. There is a set $u$ with $(u,v)\in F$; then $u\in A$ and $F(u)=v$, so $F$ is surjective.

Bijective. By Injective, Surjective and Bijective Functions between Classes §bijective, $F$ is a bijection from $A$ to $B$ if and only if $F:A\to B$ and $F$ is injective and surjective. If this holds, then $\mu(F,A,B)$ by the clause map, and $\iota(F)$ and $\sigma(F,B)$ by the clauses injective and surjective. Conversely, if $\mu(F,A,B)\wedge\iota(F)\wedge\sigma(F,B)$, then $F:A\to B$ by the clause map, and then $F$ is injective and surjective by the clauses injective and surjective.