Theorem canth2 5717

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

Hypothesis

Ref	Expression
canth2.1	|- A e. _V

Assertion

Ref	Expression
canth2	|- A ~< ~PA

Proof of Theorem canth2

Step	Hyp	Ref	Expression
1		brsdom 5601	. 2 |- (A ~< ~PA <-> (A ~<_ ~PA /\ -. A ~~ ~PA))
2		canth2.1	. . 3 |- A e. _V
3		visset 2541	. . . . . 6 |- x e. _V
4	3	snelpw 3665	. . . . 5 |- (x e. A <-> {x} e. ~PA)
5	4	biimpi 224	. . . 4 |- (x e. A -> {x} e. ~PA)
6	3	sneqr 3335	. . . . . 6 |- ({x} = {y} -> x = y)
7		sneq 3247	. . . . . 6 |- (x = y -> {x} = {y})
8	6, 7	impbii 223	. . . . 5 |- ({x} = {y} <-> x = y)
9	8	a1i 8	. . . 4 |- ((x e. A /\ y e. A) -> ({x} = {y} <-> x = y))
10	5, 9	dom2 5625	. . 3 |- (A e. _V -> A ~<_ ~PA)
11	2, 10	ax-mp 7	. 2 |- A ~<_ ~PA
12	2	canth 5249	. . . . 5 |- -. f:A-onto->~PA
13		f1ofo 4729	. . . . 5 |- (f:A-1-1-onto->~PA -> f:A-onto->~PA)
14	12, 13	mto 151	. . . 4 |- -. f:A-1-1-onto->~PA
15	14	nex 1739	. . 3 |- -. E.f f:A-1-1-onto->~PA
16	2	pwex 3654	. . . 4 |- ~PA e. _V
17	16	bren 5597	. . 3 |- (A ~~ ~PA <-> E.f f:A-1-1-onto->~PA)
18	15, 17	mtbir 314	. 2 |- -. A ~~ ~PA
19	1, 11, 18	mpbir2an 1033	1 |- A ~< ~PA

Syntax hints:  -. wn 2   <-> wb 219   /\ wa 337   = wceq 1586   e. wcel 1588  E.wex 1615  _Vcvv 2538  ~Pcpw 3227  {csn 3238   class class class wbr 3507  -onto->wfo 4129  -1-1-onto->wf1o 4130   ~~ cen 5584   ~<_ cdom 5585   ~< csdm 5586

This theorem is referenced by:  canth2g 5718  1sdom2 5814  alephsucpw2 6234  pwsdompw 6264  numthcor 6358  alephsucpw 6434  pwcfsdom 6450  cfpwsdom 6451  infmap1 9236

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-rab 2362  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-en 5588  df-dom 5589  df-sdom 5590

Copyright terms: Public domain