Proof of Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term

Throughout, the parameters have their fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i). The set variables form an infinite list (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (i)), so as many distinct set variables as needed can be chosen outside any finitely many given formulas, terms and variables. Every formula formed below applies no quantifier to a class variable, ordered pairs in it being as in 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), so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Proof of (i). The formulas $\mu(f,N,x)$ and $\sigma(f,x)$ are 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 (vii) 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), with free variables $f$, $N$, $x$ and $f$, $x$; so $\mathrm{cnt}(x)$ is predicative, and as $a$ and $f$ are bound in it, its free variables are $x$ and $N$. Let $c$ be a set assigned to $x$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iii), $\forall a\,(a\notin c)$ holds if and only if $c=\emptyset$. 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 (vii) 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), $\exists f\,(\mu(f,N,c)\wedge\sigma(f,c))$ holds if and only if some set $f$ is a surjective map $f:\mathbb{N}\to c$; and every map $\mathbb{N}\to c$ is a set, by Sets and Maps: Ordinary Notation (v). So $\mathrm{cnt}(x)$ holds if and only if $c=\emptyset$ or there is a surjective map $\mathbb{N}\to c$, that is, by Countable Set (i), if and only if $c$ is countable.

Now let $t$ be a term of type $A$ under $\gamma$. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $t$. By Terms and Typed Terms under a Guard (iv) a predicative formula $\psi$ expresses $\gamma\wedge z=t$; its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $t$, by Conditions Expressed by a Predicative Formula, and Guards (ii). Let $\mathrm{cnt}(z)$ be formed as above with $z$ for $x$, its bound variables chosen other than $z$. The formula $\exists z\,(\psi\wedge\mathrm{cnt}(z))$ is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $N$ and the parameters of $\gamma$ and $t$. Under an assignment of sets to $x_{1},\dots,x_{k}$, by Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i), $\psi$ holds for a set assigned to $z$ if and only if $\gamma$ holds and that set is the value of $t$; so $\exists z\,(\psi\wedge\mathrm{cnt}(z))$ holds if and only if $\gamma$ holds and the value of $t$ satisfies $\mathrm{cnt}$, that is, is countable. So this formula expresses the condition, with the parameter $N$.

Proof of (ii). Values. Under an assignment satisfying $\gamma$, the set $n$ lies in $\mathbb{N}_{0}$, and $[n]$ is a set contained in $\mathbb{N}_{0}$ by The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ (i). By Tuples in a Set: the Set of n-Tuples and Their Components (i) and Tuples in a Set: the Set of n-Tuples and Their Components (ii), $S^{[n]}$ is a set whose elements are the maps $w:[n]\to S$. Let $w$ be such a map. Every element of $w$ is an ordered pair $(b,s)$ by Relations, Domain, Range, Inverse and Composition (i), with $b\in\operatorname{dom}w=[n]$ and $s\in\operatorname{ran}w\subseteq S$ by Relations, Domain, Range, Inverse and Composition (ii), Relations, Domain, Range, Inverse and Composition (iii) and Functions, Values of a Function, and Functions from One Class to Another (iii); so it lies in the set $\mathbb{N}_{0}\times S$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), and $w\in\mathcal{P}(\mathbb{N}_{0}\times S)$ by The Union Set and the Power Set of a Set (ii). Hence $S^{[n]}\subseteq\mathcal{P}(\mathbb{N}_{0}\times S)$, and $S^{[n]}\in\mathcal{P}(\mathcal{P}(\mathbb{N}_{0}\times S))$ by The Union Set and the Power Set of a Set (ii). So Terms and Typed Terms under a Guard (iii) holds.

The formula. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $S^{[n]}$; so $z$ is neither $n$ nor $S$. Let $d$ and $w$ be distinct set variables that are none of $x_{1},\dots,x_{k}$ and $z$, do not occur in $\gamma$ and are not $S$. By Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness (i), with $d$ and $n$ for its $z$ and $n$ and $N$ and $R$ for its $Y$ and $R$, there is a predicative formula $\mathrm{seg}(d,n)$, with free variables among $d$, $n$, $N$ and $R$, such that for every set $d$ and every $n\in\mathbb{N}_{0}$, $\mathrm{seg}(d,n)$ holds if and only if $d=[n]$. Let $\mu(w,d,S)$ be the formula 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) with $w$, $d$ and $S$ for its $F$, $A$ and $B$, its bound variables chosen outside the variables above, and let $\psi$ be

$$\gamma\wedge\forall w\,\bigl(w\in z\Leftrightarrow\exists d\,(\mathrm{seg}(d,n)\wedge\mu(w,d,S))\bigr).$$

It is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $S^{[n]}$. Under an assignment of sets to $x_{1},\dots,x_{k}$ and $z$: if $\gamma$ fails, $\psi$ fails. If $\gamma$ holds, then $n\in\mathbb{N}_{0}$, so for all sets $w$ and $d$, $\mathrm{seg}(d,n)$ holds if and only if $d=[n]$, by Locality of Predicative Formulas: Truth Depends Only on the Values of the Free Variables (i) and the property of $\mathrm{seg}$; hence $\exists d\,(\mathrm{seg}(d,n)\wedge\mu(w,d,S))$ holds if and only if $\mu(w,[n],S)$, 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 (vii), if and only if $w$ is a map $[n]\to S$, that is, by Tuples in a Set: the Set of n-Tuples and Their Components (ii), if and only if $w\in S^{[n]}$. So $\psi$ holds if and only if $z$ and $S^{[n]}$ have the same elements, that is, by Axiom of Extensionality for Classes, if and only if $z=S^{[n]}$. So $\psi$ expresses $\gamma\wedge z=S^{[n]}$, Terms and Typed Terms under a Guard (iv) holds, and $S^{[n]}$ is a term of type $\mathcal{P}(\mathcal{P}(\mathbb{N}_{0}\times S))$ under $\gamma$ by Terms and Typed Terms under a Guard (ii). For $k=1$, $n=x_{1}$ and $\gamma$ the formula $n\in N$, which is predicative with free variables $n$ and $N$, every assignment satisfying $\gamma$ gives $n\in\mathbb{N}\subseteq\mathbb{N}_{0}$.