1 準備

1.1 空集合、2項関数

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

word(ss,s) … \(\cup\)  \(\cap\)  \(\mathop\setminus\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \in X \mid x \in Y \}\)
∖. … \(X \mathop\setminus Y = \{ x \in X \mid x \notin Y \}\)

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 \}\)
word(ss,s) … *^ap
*^ap. … \(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)
\(R(A)\) は \(A\) の \(R\) による像。主定理の説明では \(R[A]\) と書く。

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 = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)

word(ss,p) … \(\stackrel{\#}=\)  \(\stackrel{\#}\le\)
=#. … \(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\)

word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)

2 主定理

単射 \(f : X \to Y\)、\(g : Y \to X\) に対して \(\Phi(B) = (X \setminus g[Y]) \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