Theorem canth2 4627

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

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 4520	. 2 |- (A ~< P~A <-> (A ~<_ P~A /\ -. A ~~ P~A))
2		canth2.1	. . 3 |- A e. V
3		visset 1858	. . . . . 6 |- x e. V
4	3	snelpw 2832	. . . . 5 |- (x e. A <-> {x} e. P~A)
5	4	biimpi 149	. . . 4 |- (x e. A -> {x} e. P~A)
6	3	sneqr 2541	. . . . . 6 |- ({x} = {y} -> x = y)
7		sneq 2474	. . . . . 6 |- (x = y -> {x} = {y})
8	6, 7	impbii 155	. . . . 5 |- ({x} = {y} <-> x = y)
9	8	a1i 8	. . . 4 |- ((x e. A /\ y e. A) -> ({x} = {y} <-> x = y))
10	5, 9	dom2 4544	. . 3 |- (A e. V -> A ~<_ P~A)
11	2, 10	ax-mp 7	. 2 |- A ~<_ P~A
12	2	canth 4203	. . . . 5 |- -. f:A-onto->P~A
13		f1ofo 3802	. . . . 5 |- (f:A-1-1-onto->P~A -> f:A-onto->P~A)
14	12, 13	mto 105	. . . 4 |- -. f:A-1-1-onto->P~A
15	14	nex 1136	. . 3 |- -. E.f f:A-1-1-onto->P~A
16	2	pwex 2822	. . . 4 |- P~A e. V
17	16	bren 4516	. . 3 |- (A ~~ P~A <-> E.f f:A-1-1-onto->P~A)
18	15, 17	mtbir 190	. 2 |- -. A ~~ P~A
19	1, 11, 18	mpbir2an 734	1 |- A ~< P~A

Syntax hints:  -. wn 2   <-> wb 144   /\ wa 221   = wceq 991   e. wcel 993  E.wex 1015  Vcvv 1856  P~cpw 2457  {csn 2466   class class class wbr 2691  -onto->wfo 3260  -1-1-onto->wf1o 3261   ~~ cen 4503   ~<_ cdom 4504   ~< csdm 4505

This theorem is referenced by:  canth2g 4628  1sdom2 4670  numthcor 4930  alephsucpw 5018  infmap1 7783

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-pow 2817  ax-pr 2854  ax-un 3088

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-rab 1697  df-v 1857  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2458  df-sn 2469  df-pr 2470  df-op 2473  df-uni 2569  df-br 2692  df-opab 2740  df-id 2912  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-f1 3275  df-fo 3276  df-f1o 3277  df-fv 3278  df-en 4507  df-dom 4508  df-sdom 4509

Copyright terms: Public domain