\(X\) から \(Y\) への単射と \(Y\) から \(X\) への単射があれば、\(X\) と \(Y\) の間に全単射がある。

1 準備

「単射」は定義せず、次を使う。
word(ss,p) … \(\stackrel{\#}\le\)
≤#. … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists A \subset Y . X \stackrel{\#}= A\)

2 主定理

2.1 証明①

最小の不動点を作る証明。
部分集合 \(Y' \subset Y\)、\(X' \subset X\) と全単射 \(f : X \to Y'\)、\(g : Y \to X'\) に対して \(\Phi(B) = (X \setminus X') \cup g[f[B]]\) とする。
\(\Phi(B) \subset B\) を満たす集合 \(B\) すべてに属する \(X\) の元を集めて \(A\) とする（\(B = X\) が候補の1つ）。
\(\Phi\) は包含を保つ。各候補 \(B\) で \(A \subset B\)，\(\Phi(A) \subset \Phi(B) \subset B\) より \(\Phi(A) \subset A\)。
もう一度包含を保つことから \(\Phi(A)\) も候補になり \(A \subset \Phi(A)\)。
よって \(\Phi(A) = A\) で、\(g\) の単射性から \(g(y) \in A \iff y \in f[A]\)。
\(A\) の上では \(f\)、\(X \setminus A\) の上では \(g\) の逆を使って \(f' : X \to Y\) を作る。
\(f'\) は \(A\) を \(f[A]\) へ、\(X \setminus A\) を \(Y \setminus f[A]\) へ全単射に移す。
\(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

2.2 証明②

証明①と同じく、閉じた最小の集合を作る証明（Dedekind）。
まず \(Z \subset X\) かつ \(X \le^{\#} Z\) なら、\(X\) と \(Z\) は同じ大きさであることを示す。
部分集合 \(Z' \subset Z\) への全単射 \(h : X \to Z'\) を取り、\(X \setminus Z\) を含み \(h\) で閉じた最小の集合を \(A\) とする。\(A = (X \setminus Z) \cup h[A]\)。
\(A\) の上では \(h\)、\(X \setminus A\) の上では恒等写像として \(k : X \to Z\) を作ると、\(k\) は全単射になる。
\(Z \subset X , X \stackrel{\#}\le Z \Longrightarrow X \stackrel{\#}= Z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

部分集合 \(Y' \subset Y\)、\(X' \subset X\) と全単射 \(f : X \to Y'\)、\(g : Y \to X'\) を取る。
\(g \circ f\) は \(X\) から \(g[Y'] \subset X'\) への全単射なので \(X \le^{\#} X'\)。上の結果から \(X\) と \(X'\) は同じ大きさになる。
\(g\) によって \(Y\) と \(X'\) も同じ大きさなので、\(X\) と \(Y\) は同じ大きさになる。
\(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s