Theorem canth2 5359

Description: Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 4923.

Hypothesis

Ref	Expression
canth2.1	|- A e. _V

Assertion

Ref	Expression
canth2	|- A ~< ~PA

Proof of Theorem canth2

Step	Hyp	Ref	Expression
1		brsdom 5251	. 2 |- (A ~< ~PA <-> (A ~<_ ~PA /\ -. A ~~ ~PA))
2		canth2.1	. . 3 |- A e. _V
3		visset 2128	. . . . . 6 |- x e. _V
4	3	snelpw 3316	. . . . 5 |- (x e. A <-> {x} e. ~PA)
5	4	biimpi 167	. . . 4 |- (x e. A -> {x} e. ~PA)
6	3	sneqr 2969	. . . . . 6 |- ({x} = {y} -> x = y)
7		sneq 2878	. . . . . 6 |- (x = y -> {x} = {y})
8	6, 7	impbii 173	. . . . 5 |- ({x} = {y} <-> x = y)
9	8	a1i 8	. . . 4 |- ((x e. A /\ y e. A) -> ({x} = {y} <-> x = y))
10	5, 9	dom2 5275	. . 3 |- (A e. _V -> A ~<_ ~PA)
11	2, 10	ax-mp 7	. 2 |- A ~<_ ~PA
12	2	canth 4923	. . . . 5 |- -. f:A-onto->~PA
13		f1ofo 4454	. . . . 5 |- (f:A-1-1-onto->~PA -> f:A-onto->~PA)
14	12, 13	mto 120	. . . 4 |- -. f:A-1-1-onto->~PA
15	14	nex 1294	. . 3 |- -. E.f f:A-1-1-onto->~PA
16	2	pwex 3302	. . . 4 |- ~PA e. _V
17	16	bren 5247	. . 3 |- (A ~~ ~PA <-> E.f f:A-1-1-onto->~PA)
18	15, 17	mtbir 208	. 2 |- -. A ~~ ~PA
19	1, 11, 18	mpbir2an 797	1 |- A ~< ~PA

Syntax hints:  -. wn 2   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  E.wex 1164  _Vcvv 2125  ~Pcpw 2856  {csn 2868   class class class wbr 3158  -onto->wfo 3807  -1-1-onto->wf1o 3808   ~~ cen 5234   ~<_ cdom 5235   ~< csdm 5236

This theorem is referenced by:  canth2g 5360  1sdom2 5429  numthcor 5744  alephsucpw 5814  infmap1 8637

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-id 3401  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-en 5238  df-dom 5239  df-sdom 5240

Copyright terms: Public domain