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

This helper adopts the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices; it is a statement of the metatheory about formulas and expressions, predicative being meant for formulas written with abbreviations. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters with their fixed values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards (i); let $\gamma$ be a guard; and let terms under $\gamma$ and their values, terms of type $A$ under $\gamma$ for a class $A$, and conditions expressed by a predicative formula be as in Terms and Typed Terms under a Guard (i), Terms and Typed Terms under a Guard (ii) and Conditions Expressed by a Predicative Formula, and Guards (ii). Countable sets are as in Countable Set (i). For a set $S$ and $n\in\mathbb{N}_{0}$, $S^{[n]}$ is the set of maps $[n]\to S$ of Tuples in a Set: the Set of n-Tuples and Their Components (i), with $[n]$ as in Intervals of Natural Numbers (ii). Let $N$ and $R$ be class variables, parameters with the values $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$.

(i) Let $x$, $a$ and $f$ be distinct set variables, let $\mu(f,N,x)$ and $\sigma(f,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 (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 $f$, $N$ and $x$ for their $F$, $A$ and $B$, their bound variables chosen other than $x$, $a$ and $f$, and let $\mathrm{cnt}(x)$ be the formula

$$\forall a\,(a\notin x)\vee\exists f\,\bigl(\mu(f,N,x)\wedge\sigma(f,x)\bigr).$$

It is predicative, its free variables are $x$ and $N$, and for every set $c$, $\mathrm{cnt}(x)$ holds when $c$ is assigned to $x$ if and only if $c$ is countable. Consequently, for every class $A$ and every term $t$ of type $A$ under $\gamma$, the condition $\gamma\wedge$ "the set $t$ is countable" on $x_{1},\dots,x_{k}$ is expressed by a predicative formula.

(ii) Let $S$ be a parameter whose value is a set, also written $S$, and let $n$ be one of $x_{1},\dots,x_{k}$ such that $n\in\mathbb{N}_{0}$ under every assignment satisfying $\gamma$. Let $S^{[n]}$ be the term under $\gamma$, written with $n$ and the parameters $S$, $N$ and $R$, whose value under each assignment satisfying $\gamma$ is $S^{[n]}$ for the set assigned to $n$. Then $S^{[n]}$ is a term of type $\mathcal{P}(\mathcal{P}(\mathbb{N}_{0}\times S))$ under $\gamma$, with the power set $\mathcal{P}$ and the Cartesian product $\times$. For instance, $k=1$, $n=x_{1}$ and $\gamma$ the formula $n\in N$ qualify, as $\mathbb{N}\subseteq\mathbb{N}_{0}$.