どの集合 \(X\) も、そのべき集合 \(℘X\) より真に小さい。

1 準備

word(ss,p) … \(\stackrel{\#}\le\)  \(\stackrel{\#}<\)
≤#. … \(X \stackrel{\#}\le Y \Longleftrightarrow \exists A \subset Y . X \stackrel{\#}= A\)
<#. … \(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \stackrel{{\tt /}}{\stackrel{\#}=} Y\)
一元集合の族 \(A = \{\{x\} \mid x \in X\}\) は \(\wp X\) の部分集合で、\(x \mapsto \{x\}\) は \(X\) と \(A\) の全単射になる。
\(X \stackrel{\#}\le \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf \(\mathrm{S}\) := \(\{ \{ x \} \mid x \in \mathrm{X} \}\) ; LS <- \(\mathrm{S} \subset \wp \mathrm{X}\) // \(\mathbb{W}.\)'!=. -| set1. p;
hyS <- \(\mathrm{S} = \mathrm{S}\) ;
\(\mathrm{g}\) := \(\{ \langle x , \{ x \} \rangle \mid x \in \mathrm{X} \}\) ; \(\mathrm{g} \subset \mathrm{X} \times \mathrm{S}\) // \(\mathbb{W}.\)'!=. -| hyS , set1. p;
LG <- \(\mathrm{g} \in \mathrm{X} \stackrel{\rm IS}\to \mathrm{S}\) /// \(\mathbb{W}.\)'!=. -| hyS , \(\mathrm{g} = \mathrm{g}\) , pr:0 , set1. p;
\(\mathrm{X} \stackrel{\#}\le \wp \mathrm{X}\) // \(\mathbb{W}.\)'!=. -| LG , hyS , LS p;
goal -| \(\mathbb{W}.\) , ax_s h[fix];

2 主定理

2.1 証明①

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\) となって矛盾する（対角線論法）。
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf \(\mathrm{A}\) := \(\{ x \in \mathrm{X} \mid \not\exists y \, ( \langle x , y \rangle \in \mathrm{f} , x \in y ) \}\) ;
\(\mathrm{f} \notin \mathrm{X} \stackrel{\rm IS}\to \wp \mathrm{X}\) //// \(\mathbb{W}.\) -| ax_s[\(C\):=\(\mathrm{A}\)] , pr:0 v;
Le <- \(f \notin X \stackrel{\rm IS}\to \wp X\) -| \(\mathbb{W}.\) , ax_s h[fix];
goal / <#. / =#.' -| \(X \stackrel{\#}\le \wp X\) , Le p;
goal -| \(\mathbb{W}.\) , ax_s h;
forget}

2.2 証明②

forget{
全単射 \(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\)。どちらも矛盾する。
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
prf \(\mathrm{B}\) := \(\{ x \in \mathrm{X} \mid \exists A \, ( \langle A , x \rangle \in \mathrm{g} , x \notin A ) \}\) ;
\(\mathrm{g} \notin \wp \mathrm{X} \stackrel{\rm IS}\to \mathrm{X}\) //// \(\mathbb{W}.\) -| ax_s[\(C\):=\(\mathrm{B}\)] , pr:0 v;
Le <- \(g \notin \wp X \stackrel{\rm IS}\to X\) -| \(\mathbb{W}.\) , ax_s h[fix];
goal / <#. / =#.' -| \(X \stackrel{\#}\le \wp X\) , Le , →IS^sw p;
goal -| \(\mathbb{W}.\) , ax_s h;
forget}
!txt 2026-10-23 実験：≤#. を「Y の部分集合と同じ大きさ」で定義。X ≤# ℘ X は一元集合の族との全単射で示す（hyS・hyg で集合を固定し、存在は h[fix] で処理）。主定理は正方向・逆方向の全単射をそれぞれ直接否定し、単射・全射の記号とその補題を省いた。