可算集合

$S$ が有限でないとする。$\mathbb{N}$ から $S$ への狭義単調増加な全単射を構成する。
$n\in\mathbb{N}$ に対し $S_n:=S\setminus\{f(0),\dots,f(n-1)\}$ とおき（$S_0=S$）、$f\colon\mathbb{N}\to\mathbb{N}$ を再帰で
$$ f(n):=\begin{cases}\min S_n,& S_n\ne\emptyset,\\ 0,& S_n=\emptyset\end{cases} $$
と定める（$S_n$ は $f(0),\dots,f(n-1)$ だけから決まるので、この再帰は正しく定義される。空でない $S_n$ の最小元は $\mathbb{N}$ の整列性により存在する）。
次の主張 $P(n)$ を $n$ に関する帰納法で示す：$S_n\ne\emptyset$ であり、$f(0),\dots,f(n)$ はすべて $S$ に属し、$f(0)< f(1)<\dots< f(n)$ である。
$P(0)$：$S_0=S$ は空でない（空集合は $[0]$ と対等なので有限だが、$S$ は有限でない）ので $f(0)=\min S\in S$ である。
$P(n)\Rightarrow P(n+1)$：$P(n)$ により $f(0)<\dots< f(n)$ は $S$ の相異なる元である。もし $S_{n+1}=\emptyset$ なら $S\subset\{f(0),\dots,f(n)\}$ であり、逆の包含も成り立つので $S=\{f(0),\dots,f(n)\}$ となる。すると $k\mapsto f(k)$ は $[n+1]$ から $S$ への全単射（単射性は狭義単調性から）であり、$S$ が有限になって仮定に反する。よって $S_{n+1}\ne\emptyset$ であり、$f(n+1)=\min S_{n+1}\in S_{n+1}\subset S$ である。$f(n+1)\in S_{n+1}\subset S_n$ と $f(n)=\min S_n$ から $f(n)\le f(n+1)$ であり、$f(n+1)\notin\{f(0),\dots,f(n)\}$ から $f(n)\ne f(n+1)$ なので $f(n)< f(n+1)$ である。これで $P(n+1)$ が示された。
以上により $f$ は $\mathbb{N}$ から $S$ への狭義単調増加写像であり、特に単射である。また $f(n)\ge n$ が帰納法で従う（$f(0)\ge0$、$f(n+1)>f(n)\ge n$ より $f(n+1)\ge n+1$）。
$f$ が $S$ への全射であることを示す。$s\in S$ が $f$ の像に属さないとすると、すべての $n$ について $s\in S_n$ なので $f(n)=\min S_n\le s$ である。ところが $f(s+1)\ge s+1>s$ であり矛盾する。よって $f\colon\mathbb{N}\to S$ は全単射であり、$S$ は可算無限である。$\square$

まず、$A$ が可算なら $A$ から $\mathbb{N}$ への単射 $g$ が存在することに注意する。$A$ が有限なら全単射 $v\colon[n]\to A$ があり、その逆写像 $v^{-1}\colon A\to[n]$ と包含 $[n]\subset\mathbb{N}$ の合成が単射 $g$ である。$A$ が可算無限なら番号付け $e\colon\mathbb{N}\to A$ の逆写像が $g$ である。
1：$g$ の $B$ への制限（写像の制限）$g|_B$ は $B$ から $S:=g(B)\subset\mathbb{N}$ への全単射である。lem-countable-set-subsets により $S$ は有限または可算無限である。$S$ が有限で $w\colon[m]\to S$ が全単射なら $(g|_B)^{-1}\circ w\colon[m]\to B$ が全単射であり $B$ は有限である。$S$ が可算無限で $w\colon\mathbb{N}\to S$ が全単射なら、同様に $B$ は可算無限である。いずれにせよ $B$ は可算である。
2：$A$ が有限で $v\colon[n]\to A$ が全単射のとき、上の $g$ について $S=g(B)\subset[n]$ である。「$[n]$ の任意の部分集合は有限である」を $n$ に関する帰納法で示す。$n=0$ のとき $[0]=\emptyset$ の部分集合は $\emptyset$ だけであり有限である。$[n]$ について成り立つとし、$T\subset[n+1]$ とする。$T':=T\cap[n]$ は $[n]$ の部分集合なので有限であり、全単射 $u\colon[m]\to T'$ がある。$n\notin T$ なら $T=T'$ は有限である。$n\in T$ なら $T=T'\cup\{n\}$（互いに素な和）であり、$u'\colon[m+1]\to T$ を $k< m$ に対して $u'(k):=u(k)$、$u'(m):=n$ で定めると全単射である。よって $T$ は有限である。したがって $S$ は有限であり、1 と同じ合成により $B$ も有限である。$\square$

1 ⇒ 2：prf-countable-set-subset の冒頭で示した。
2 ⇒ 1：$g\colon A\to\mathbb{N}$ を単射とする。$g$ は $A$ から $g(A)\subset\mathbb{N}$ への全単射であり、lem-countable-set-subsets により $g(A)$ は有限または可算無限である。全単射を合成すれば、$A$ もそれぞれ有限または可算無限である。
2 ⇒ 3：$g\colon A\to\mathbb{N}$ を単射とし、$A\ne\emptyset$ なので元 $a_0\in A$ を一つ固定する。$h\colon\mathbb{N}\to A$ を、$n\in g(A)$ のときは $g(a)=n$ となる唯一の $a$ を $h(n)$ とし、$n\notin g(A)$ のときは $h(n):=a_0$ として定める。任意の $a\in A$ に対して $h(g(a))=a$ なので $h$ は全射である。
3 ⇒ 2：$h\colon\mathbb{N}\to A$ を全射とする。各 $a\in A$ に対し、逆像 $h^{-1}(\{a\})$ は $\mathbb{N}$ の空でない部分集合なので最小元をもつ。$g(a):=\min h^{-1}(\{a\})$ とおく。$h(g(a))=a$ なので、$g(a)=g(b)$ ならば $a=h(g(a))=h(g(b))=b$ であり、$g$ は単射である。ここで各 $a$ に対する $g(a)$ は最小元という規則で一意に決まっているので、選択公理は使っていない。$\square$

1：$A=\emptyset$ なら $f(A)=\emptyset$ は有限である。$A\ne\emptyset$ なら prop-countable-set-characterization により全射 $e\colon\mathbb{N}\to A$ があり、$f\circ e\colon\mathbb{N}\to f(A)$ は全射である。$f(A)\ne\emptyset$ なので再び prop-countable-set-characterization により $f(A)$ は可算である。
2：$g$ は $A$ から $g(A)\subset B$ への全単射であり、prop-countable-set-subset の 1 により $g(A)$ は可算である。全単射の合成により $A$ も可算である。$\square$

$2^{m}(2n+1)\ge1$ なので $\pi$ の値は自然数である。
全射性：任意の正の整数 $N$ が $N=2^{m}(2n+1)$（$m,n\in\mathbb{N}$）と書けることを、$N$ に関する強い帰納法で示す。$N$ が奇数なら $N=2^{0}(2n+1)$、$n=(N-1)/2$ である。$N$ が偶数なら $N=2N'$、$1\le N'< N$ であり、帰納法の仮定により $N'=2^{m'}(2n+1)$ なので $N=2^{m'+1}(2n+1)$ である。よって任意の自然数 $k$ に対し $k+1=2^{m}(2n+1)$ となる $(m,n)$ があり、$\pi(m,n)=k$ である。
単射性：$2^{m}(2n+1)=2^{m'}(2n'+1)$ とする。$m< m'$ なら両辺を $2^{m}$ で割って $2n+1=2^{m'-m}(2n'+1)$ となるが、左辺は奇数、右辺は $m'-m\ge1$ により偶数であり矛盾する。$m>m'$ も同様に矛盾する。よって $m=m'$ であり、$2n+1=2n'+1$ から $n=n'$ である。$\square$

$A=\emptyset$ または $B=\emptyset$ なら $A\times B=\emptyset$ は有限である。そうでなければ prop-countable-set-characterization により全射 $e\colon\mathbb{N}\to A$、$e'\colon\mathbb{N}\to B$ がある。写像 $\mathbb{N}\times\mathbb{N}\to A\times B$、$(m,n)\mapsto(e(m),e'(n))$ は全射であり、これを prop-countable-set-pairs の全単射の逆写像 $\pi^{-1}\colon\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ と合成すると $\mathbb{N}$ から $A\times B$ への全射が得られる。よって $A\times B$ は可算である。
$k$ 個の直積については、$A_1\times\cdots\times A_{k+1}$ を $(A_1\times\cdots\times A_k)\times A_{k+1}$ と同一視して $k$ に関する帰納法を用いればよい。$\square$

$A:=\bigcup_{n\in\mathbb{N}}A_n$、$I:=\{n\in\mathbb{N}\mid A_n\ne\emptyset\}$ とおく。$I=\emptyset$ なら $A=\emptyset$ は有限である。以下 $I\ne\emptyset$ とし、$n_0\in I$ を一つ固定する。
各 $n\in I$ に対し、$\mathbb{N}$ から $A_n$ への全射全体の集合を $E_n$ とおく。$A_n$ は空でない可算集合なので、prop-countable-set-characterization により $E_n\ne\emptyset$ である。添字集合を $\mathbb{N}$ にそろえるため、$n\in I$ に対して $E'_n:=E_n$、$n\notin I$ に対して $E'_n:=E_{n_0}$ とおく。空でない集合の族 $(E'_n)_{n\in\mathbb{N}}$ に可算選択公理を適用すると、各 $n\in\mathbb{N}$ に対して $e_n\in E'_n$ を対応させる族 $(e_n)_{n\in\mathbb{N}}$ が存在する。すなわち、$n\in I$ のとき $e_n\colon\mathbb{N}\to A_n$ は全射であり、$n\notin I$ のとき $e_n\colon\mathbb{N}\to A_{n_0}$ は全射である。
写像 $F\colon\mathbb{N}\times\mathbb{N}\to A$ を $F(n,k):=e_n(k)$ で定める（$e_n$ の値はつねに $A_n$ または $A_{n_0}$ に属し、いずれも $A$ の部分集合である）。$F$ は全射である。実際、$a\in A$ とすると $a\in A_n$ となる $n$ があり、このとき $A_n\ne\emptyset$ なので $n\in I$ であり、$e_n$ の全射性から $e_n(k)=a$ となる $k$ がある。$F$ を prop-countable-set-pairs の逆写像 $\pi^{-1}\colon\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ と合成すれば $\mathbb{N}$ から $A$ への全射が得られ、$A\ne\emptyset$ なので prop-countable-set-characterization により $A$ は可算である。
有限個の和については、$n< k$ に対して $A'_n:=A_n$、$n\ge k$ に対して $A'_n:=\emptyset$ とおけば $A_0\cup\cdots\cup A_{k-1}=\bigcup_{n\in\mathbb{N}}A'_n$ であり、上の議論が使える。この場合 $I\subset[k]$ は有限なので、$n\in I$ について全射 $e_n$ を選び、$n\notin I$ については $e_n:=e_{n_0}$ とおけばよい。全射を選ぶのは有限個の $n$ についてだけなので、可算選択公理は不要である（有限個の存在命題から有限個の対象を同時に取り出すことは、個数に関する帰納法により選択公理なしで正当化される）。$\square$

$f\colon A\to\mathcal{P}(A)$ を任意の写像とし、
$$ D:=\{a\in A\mid a\notin f(a)\}\in\mathcal{P}(A) $$
とおく。$D$ が $f$ の像に属するとして $D=f(a_0)$ とする。$a_0\in D$ ならば $D$ の定義により $a_0\notin f(a_0)=D$ であり、$a_0\notin D$ ならば $a_0\notin f(a_0)$ なので $D$ の定義により $a_0\in D$ である。いずれも矛盾するので、$D$ は $f$ の像に属さず、$f$ は全射でない。$\square$

$\mathcal{P}(\mathbb{N})$ が可算だとすると、空でないので prop-countable-set-characterization により $\mathbb{N}$ から $\mathcal{P}(\mathbb{N})$ への全射が存在し、thm-countable-set-cantor に反する。
$X\subset\mathbb{N}$ にその指示関数 $\chi_X\colon\mathbb{N}\to\{0,1\}$（$n\in X$ のとき $1$、そうでないとき $0$）を対応させる写像 $\mathcal{P}(\mathbb{N})\to\{0,1\}^{\mathbb{N}}$ は、$s\mapsto s^{-1}(\{1\})$ を逆写像にもつ全単射である。よって $\{0,1\}^{\mathbb{N}}$ が可算なら $\mathcal{P}(\mathbb{N})$ も可算になり（cor-countable-set-image の 2）矛盾する。$\square$

部分和は単調増加で、$\sum_{n=0}^{N}d_n10^{-(n+1)}\le8\sum_{j\ge1}10^{-j}=8/9$ により上に有界なので、級数は収束し $0< x\le8/9$ である。
$n\in\mathbb{N}$ を固定する。
$$ 10^{n+1}x=\sum_{k=0}^{n}d_k10^{n-k}+r_n,\qquad r_n:=\sum_{k=n+1}^{\infty}d_k10^{n-k} $$
と書ける。右辺の有限和 $M_n:=\sum_{k=0}^{n}d_k10^{n-k}$ は自然数であり、$r_n$ については
$$ 0< r_n\le8\sum_{k=n+1}^{\infty}10^{n-k}=8\sum_{j=1}^{\infty}10^{-j}=\frac{8}{9}<1 $$
である。よって $M_n\le10^{n+1}x< M_n+1$ であり、$\lfloor10^{n+1}x\rfloor=M_n$ である。
$n\ge1$ のとき、同じことを $n-1$ について行えば $\lfloor10^{n}x\rfloor=M_{n-1}=\sum_{k=0}^{n-1}d_k10^{n-1-k}$ である。$n=0$ のときは $0< x\le8/9$ から $\lfloor x\rfloor=0$ であり、これは空和 $M_{-1}:=0$ と一致する。したがって
$$ \delta_n(x)=M_n-10M_{n-1}=\sum_{k=0}^{n}d_k10^{n-k}-\sum_{k=0}^{n-1}d_k10^{n-k}=d_n $$
である。$\square$

$h\colon\mathbb{N}\to\mathbb{R}$ を任意の写像とし、$x_n:=h(n)$ とおく。lem-countable-set-digits の記号 $\delta_n$ を用いて、自然数の列 $(d_n)_{n\in\mathbb{N}}$ を
$$ d_n:=\begin{cases}2,& \delta_n(x_n)=1,\\ 1,& \delta_n(x_n)\ne1\end{cases} $$
で定める。各 $n$ について $d_n\in\{1,2\}$ かつ $d_n\ne\delta_n(x_n)$ である。$x:=\sum_{n=0}^{\infty}d_n10^{-(n+1)}$ とおくと、lem-countable-set-digits により級数は収束し、$0< x\le8/9<1$ であり、すべての $n$ について $\delta_n(x)=d_n$ である。
$x$ が $h$ の像に属さないことを示す。$x=x_n$ となる $n$ があったとすると、$\delta_n$ は実数だけで決まる量なので $\delta_n(x)=\delta_n(x_n)$ である。ところが左辺は $d_n$ であり、$d_n\ne\delta_n(x_n)$ なので矛盾する。よって任意の $n$ について $x\ne h(n)$ である。
特に $\mathbb{N}$ から $\mathbb{R}$ への全射は存在しない。$\mathbb{R}\ne\emptyset$ なので、prop-countable-set-characterization により $\mathbb{R}$ は可算でない。$\square$