1 準備

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

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
!prop/thm ∅.' … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf ∅.' // W. -| O p; ∅.' -| W. h;

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 \}\)
!prop/thm ℘.' … \(\wp X = \{ A \mid \forall a \in A . a \in X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf ℘.' -| W. p;

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}.\)
prf pr:0 -| ◁. , ▷. p;
pr:0 -| W. h;

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 \}\)
!prop/thm →.' … \(X \to Y = \{ f \mid \forall p \in f . \exists x \in X . \exists y \in Y . p = \langle x , y \rangle , \forall x \in X . \exists! y \langle x , y \rangle \in f \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf →.' /// W.!=. -| O p; →.' -| W. h;
→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\)
!prop/thm =#.' … \(X \stackrel{\#}= Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm IS}\to Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
!prop/thm ≤#.' … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists f \, f \in X \stackrel{\rm I}\to Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h;

\(x \mapsto \{x\}\) は \(X\) から \(\wp X\) への単射になる。
\(X \stackrel{\#}\le \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf |g_ := \(\{ \langle x , \{ x \} \rangle \mid x \in \mathrm{X} \}\) ;
hyG <- \(\mathrm{g} = \mathrm{g}\) ;
Leg <- \(\mathrm{g} \subset \mathrm{X} \times \wp \mathrm{X}\) // W.'!=. -| set1. p;
LeI <- \(\mathrm{g} \in \mathrm{X} \stackrel{\rm I}\to \wp \mathrm{X}\) /// W.'!=. -| hyG /// W.'!=. , pr:0 , set1. p;
\(\mathrm{X} \stackrel{\#}\le \wp \mathrm{X}\) / ≤#.' -| LeI p;
goal -| W. , ax_s h[fix];

2 証明①

forget{
写像 \(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
prf A_ := \(\{ x \in \mathrm{X} \mid \not\exists y \, ( \langle x , y \rangle \in \mathrm{f} , x \in y ) \}\) ;
hyA <- \(\mathrm{A} = A\) ;
LAs <- \(A \subset \mathrm{X}\) -| O p;
LeA <- \(\mathrm{f} \in \mathrm{X} \to \wp \mathrm{X} \Longrightarrow \mathrm{f} \notin \mathrm{X} \stackrel{\rm S}\to \wp \mathrm{X}\) / →S. / W.' -| hyA , pr:0 v;
Lgen <- \(f \in X \to \wp X \Longrightarrow f \notin X \stackrel{\rm S}\to \wp X\) -| W. , ax_s h[fix];
goal / =#.' / →IS. / →I. -| Lgen p;
goal -| W. , ax_s h;

2つの結果を合わせると、\(\wp X\) は \(X\) より真に大きい。
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf \(\mathrm{X} \stackrel{\#}< \wp \mathrm{X}\) / <#. -| \(X \stackrel{\#}\le \wp X\) , \(X \stackrel{{\tt /}}{\stackrel{\#}=} \wp X\) p;
goal -| W. , ax_s h[fix];
forget}

3 証明②

forget{
word(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \(R ^{\hat\leftrightarrow} = \{ \langle y , x \rangle \mid \langle x , y \rangle \in R \}\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
prf →IS^sw //// W.'!=. -| pr:0 p; →IS^sw -| W. h;

単射 \(g : \wp X \to X\) に対して \(B = \{g(A) \mid A \subset X , g(A) \notin A\}\) とすると \(B \in \wp X\)。
\(g(B) \in B\) なら \(g(B) = g(A)\)、\(g(A) \notin A\) となる \(A\) があり、単射だから \(A = B\) で \(g(B) \notin B\)。
\(g(B) \notin B\) なら \(A = B\) として \(g(B) \in B\)。どちらも矛盾する。
\(\wp X \stackrel{{\tt /}}{\stackrel{\#}\le} X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf B_ := \(\{ x \in \mathrm{X} \mid \exists A \, ( \langle A , x \rangle \in \mathrm{g} , x \notin A ) \}\) ;
hyB <- \(\mathrm{B} = B\) ;
LBs <- \(B \subset \mathrm{X}\) -| O p;
LBp <- \(\mathrm{B} \in \wp \mathrm{X}\) / W.' -| hyB p;
LeB <- \(\mathrm{g} \notin \wp \mathrm{X} \stackrel{\rm I}\to \mathrm{X}\) / →I. / W.' -| LBp , hyB , pr:0 p;
Lgen <- \(g \notin \wp X \stackrel{\rm I}\to X\) -| W. , ax_s h[fix];
goal / ≤#.' -| Lgen p;
goal -| W. , ax_s h;

全単射 \(f : X \to \wp X\) があれば逆 \(f^{-1}\) は \(\wp X\) から \(X\) への全単射になるので、2つの結果を合わせると \(\wp X\) は \(X\) より真に大きい。
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf goal / <#. / =#.' -| \(X \stackrel{\#}\le \wp X\) , \(\wp X \stackrel{{\tt /}}{\stackrel{\#}\le} X\) / ≤#.' , →IS^sw , →IS. p;
goal -| W. , ax_s h;
forget}