Solution (source code)

= Solution

Use “countable” to include finite and empty sets: a <countable set> admits an <injection> into $\mathbb N_0$. If $B\subseteq A$ and $j:A\to\mathbb N_0$ is <injective>, restricting $j$ to $B$ proves that $B$ is a <countable set>.

For a <countable union of countable sets>, index the family as $A_0,A_1,\ldots$ and choose an <injection> $j_i:A_i\to\mathbb N_0$ for each member. For an element $a$ of the union, let $i(a)$ be the least index containing it, and assign
$$
a\longmapsto\bigl(i(a),j_{i(a)}(a)\bigr).
$$
This is <injective>: equality of the pair gives the same set index and then the same element. Finally the <Cantor pairing function>
$$
(i,j)\longmapsto\frac{(i+j)(i+j+1)}2+j
$$
injects $\mathbb N_0^2$ into $\mathbb N_0$. \b[The union is therefore countable.] The proof uses chosen injections for the family, as in the usual set-theoretic framework with <axiom of countable choice>.