1 準備

1.1 空集合、有限集合、べき集合

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
∅.' … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)
℘ は集合の語なので、℘. は \(\{A \mid A \subset X\}\) が集合であること＝冪集合公理を含みます。

1.2 順序対、直積

word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)

word(s,s) … \(\triangleleft\)  \(\triangleright\)
◁. … \(\triangleleft \langle x , y \rangle = x\)
▷. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,s) … \(\times\)
^^pr. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)

1.3 写像、集合の大きさ比較

\(X \to Y\) は \(X\) から \(Y\) への写像全体の集合。矢印の上の I・S・IS は単射・全射・全単射を表す。
word(ss,s) … \(\to\)  \(\stackrel{\rm I}\to\)  \(\stackrel{\rm S}\to\)  \(\stackrel{\rm IS}\to\)
→. … \(X \to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f \}\)
→I. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)
→S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\)
→IS. … \(X \stackrel{\rm IS}\to Y = \{ f \mid f \in X \stackrel{\rm I}\to Y , f \in X \stackrel{\rm S}\to Y \}\)

word(ss,p) … \(\stackrel{\#}=\)  \(\stackrel{\#}\le\)  \(\stackrel{\#}<\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)
≤#. … \(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\)
<#. … \(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \stackrel{{\tt /}}{\stackrel{\#}=} Y\)

2 主定理

\(x \mapsto \{x\}\) は \(X\) から \(\wp X\) への単射になる。
\(X \stackrel{\#}\le \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

写像 \(f : X \to \wp X\) に対して \(A = \{x \in X \mid x \notin f(x)\}\) とすると \(A \in \wp X\)。
\(A = f(a)\) となる \(a \in X\) があれば \(a \in A \iff a \notin A\) となって矛盾する（対角線論法）。
よって \(f\) は全射でなく、特に全単射は無い。
\(X \stackrel{{\tt /}}{\stackrel{\#}=} \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

2つの結果を合わせると、\(\wp X\) は \(X\) より真に大きい。
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s