Theorem canth2 4418

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 3846.

Hypothesis

Ref	Expression
canth2.1	|- A e. V

Assertion

Ref	Expression
canth2	|- A ~< P~A

Proof of Theorem canth2

Step	Hyp	Ref	Expression
1		brsdom 4317	. 2 |- (A ~< P~A <-> (A ~<_ P~A /\ -. A ~~ P~A))
2		canth2.1	. . 3 |- A e. V
3		visset 1788	. . . . . 6 |- x e. V
4	3	snelpw 2720	. . . . 5 |- (x e. A <-> {x} e. P~A)
5	4	biimp 151	. . . 4 |- (x e. A -> {x} e. P~A)
6	3	sneqr 2447	. . . . . 6 |- ({x} = {y} -> x = y)
7		sneq 2388	. . . . . 6 |- (x = y -> {x} = {y})
8	6, 7	impbi 157	. . . . 5 |- ({x} = {y} <-> x = y)
9	8	a1i 8	. . . 4 |- ((x e. A /\ y e. A) -> ({x} = {y} <-> x = y))
10	5, 9	dom2 4340	. . 3 |- (A e. V -> A ~<_ P~A)
11	2, 10	ax-mp 7	. 2 |- A ~<_ P~A
12	2	canth 3846	. . . . 5 |- -. f:A-onto->P~A
13		f1ofo 3634	. . . . 5 |- (f:A-1-1-onto->P~A -> f:A-onto->P~A)
14	12, 13	mto 106	. . . 4 |- -. f:A-1-1-onto->P~A
15	14	nex 1077	. . 3 |- -. E.f f:A-1-1-onto->P~A
16	2	pwex 2713	. . . 4 |- P~A e. V
17	16	bren 4313	. . 3 |- (A ~~ P~A <-> E.f f:A-1-1-onto->P~A)
18	15, 17	mtbir 192	. 2 |- -. A ~~ P~A
19	1, 11, 18	mpbir2an 727	1 |- A ~< P~A

Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223  E.wex 956   = wceq 1099   e. wcel 1105  Vcvv 1786  P~cpw 2372  {csn 2380   class class class wbr 2587  -onto->wfo 3143  -1-1-onto->wf1o 3144   ~~ cen 4302   ~<_ cdom 4303   ~< csdm 4304

This theorem is referenced by:  canth2g 4419  1sdom2 4457  numthcor 4710  alephsucpw 4793  pnfnre 5419  mnfnre 5420  pnfnemnf 5460  infmap1 7467

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-rab 1628  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-id 2797  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-fv 3161  df-en 4305  df-dom 4306  df-sdom 4307

Copyright terms: Public domain