Proof of Finite Powers of a Countable Set Are Countable

Throughout, $0\in\mathbb{N}_{0}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), and for $n\in\mathbb{N}_{0}$, $S^{n}$ is the set of maps $[n]\to S$ (Tuples in a Set: the Set of n-Tuples and Their Components (i), Tuples in a Set: the Set of n-Tuples and Their Components (ii)).

Step 1: $S^{0}=\{\emptyset\}$, and $S^{0}$ is countable. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $[0]=\emptyset$. The empty set has no element, so it is a relation and a function, and its domain and range are empty, by Relations, Domain, Range, Inverse and Composition (ii) and Relations, Domain, Range, Inverse and Composition (iii); so it is a map $\emptyset\to S$ by Functions, Values of a Function, and Functions from One Class to Another (iii), and $\emptyset\in S^{0}$. Conversely, let $w\in S^{0}$, so that $w$ is a map with $\operatorname{dom}w=[0]=\emptyset$. Every element of $w$ is an ordered pair $(a,b)$, by Relations, Domain, Range, Inverse and Composition (i), and then $a\in\operatorname{dom}w$ by Relations, Domain, Range, Inverse and Composition (ii), which is impossible; so $w$ has no element, and $w=\emptyset$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iii). Hence a set lies in $S^{0}$ if and only if it equals $\emptyset$, and $S^{0}=\{\emptyset\}$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (iv). This singleton is finite by The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons (iii), hence countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (iii).

Step 2: the inductive step. Let $n\in\mathbb{N}_{0}$ with $S^{n}$ countable. Then $S^{n}\times S$ is countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (vii). By Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples (vi), with $S$ for its $Y$, the map sending $(t,y)\in S^{n}\times S$ to the $(n+1)$-tuple that restricts to $t$ on $[n]$ and has the value $y$ at $n+1$ is a bijection from $S^{n}\times S$ onto $S^{n+1}$. So $S^{n+1}$ is countable by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (v).

Step 3: the induction formula. Let $N$ and $R$ be class variables whose values are $\mathbb{N}$ and the order $\le$ of $\mathbb{N}_{0}$, and let $S$ also denote a parameter with the value $S$. By Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term (ii), with $k=1$, a set variable $x$ for $x_{1}$ and $n$, and the guard $x\in N$, $S^{[x]}$ is a term of type $\mathcal{P}(\mathcal{P}(\mathbb{N}_{0}\times S))$ under that guard; so by Countability as a Predicative Condition, and Finite Powers of a Set as a Typed Term (i) the condition $\varphi(x)$, "$x\in\mathbb{N}$ and $S^{x}$ is countable", on $x$ is expressed by a predicative formula, with the parameters $N$, $R$ and $S$.

Step 4: induction. By Step 1 and Step 2 with $n=0$, $S^{0+1}$ is countable, and $0+1=1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i), as $1\in\mathbb{N}_{0}$; with $1\in\mathbb{N}$ 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 (ii), $\varphi(1)$ holds. Let $n\in\mathbb{N}$ with $\varphi(n)$. Then $n\in\mathbb{N}_{0}$ and $S^{n}$ is countable, so $S^{n+1}$ is countable by Step 2, and $n+1\in\mathbb{N}$ 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 (vi); so $\varphi(n+1)$ holds. By Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i), $\varphi(n)$ holds for every $n\in\mathbb{N}$; in particular $S^{k}$ is countable, which is (i).