Solution (source code)

= Solution

A <set> is countable if it admits an <injection> into the <natural numbers>; this includes <finite sets> and the empty <set>. Use $\mathbb N_0=\{0,1,2,\ldots\}$ for the enumeration. The <Cantor pairing function>
$$
\Pi(i,j)=\frac{(i+j)(i+j+1)}2+j
$$
is a <bijection> $\mathbb N_0^2\to\mathbb N_0$. Indeed, on the diagonal $i+j=s$, its values are the consecutive <integers> from $s(s+1)/2$ through $s(s+1)/2+s$. These intervals are disjoint, and the next starts one beyond the preceding endpoint. Every nonnegative <integer> therefore determines exactly one diagonal $s$, then exactly one $j$, and finally $i=s-j$. If one's convention starts the <natural numbers> at one, translate both coordinates by one. Thus \b[$\mathbb N\times\mathbb N$ is a <countable set>].

For <countable sets> $X,Y$, choose <injections> $e_X:X\to\mathbb N_0$ and $e_Y:Y\to\mathbb N_0$. The map $(x,y)\mapsto\Pi(e_X(x),e_Y(y))$ is an <injection>, proving their <Cartesian product> is countable. Repeating this proves that every <finite Cartesian power of a countable set> is countable.

For a sequence of <countable sets> $X_n$, choose an <injection> $e_n:X_n\to\mathbb N_0$ for each $n$. For $x\in\bigcup_nX_n$, let $n(x)$ be the least index containing $x$. The map
$$
x\longmapsto\Pi\bigl(n(x),e_{n(x)}(x)\bigr)
$$
is an <injection>: its value recovers $n(x)$ and then $x$. This proves the \b[<countable union of countable sets> theorem]. Selecting all $e_n$ uses the usual <axiom of countable choice>; if enumerations are already supplied, the construction itself needs no additional choices.