Theorem canth2

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 . This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994)

	Ref	Expression
Hypothesis	canth2.1	|- A e. _V
Assertion	canth2	|- A ~< ~P A

Proof

Step	Hyp	Ref	Expression
1		canth2.1	|- A e. _V
2	1	pwex	|- ~P A e. _V
3		snelpwi	|- ( x e. A -> { x } e. ~P A )
4		vex	|- x e. _V
5	4	sneqr	|- ( { x } = { y } -> x = y )
6		sneq	|- ( x = y -> { x } = { y } )
7	5 6	impbii	|- ( { x } = { y } <-> x = y )
8	7	a1i	|- ( ( x e. A /\ y e. A ) -> ( { x } = { y } <-> x = y ) )
9	3 8	dom3	|- ( ( A e. _V /\ ~P A e. _V ) -> A ~<_ ~P A )
10	1 2 9	mp2an	|- A ~<_ ~P A
11	1	canth	|- -. f : A -onto-> ~P A
12		f1ofo	|- ( f : A -1-1-onto-> ~P A -> f : A -onto-> ~P A )
13	11 12	mto	|- -. f : A -1-1-onto-> ~P A
14	13	nex	|- -. E. f f : A -1-1-onto-> ~P A
15		bren	|- ( A ~~ ~P A <-> E. f f : A -1-1-onto-> ~P A )
16	14 15	mtbir	|- -. A ~~ ~P A
17		brsdom	|- ( A ~< ~P A <-> ( A ~<_ ~P A /\ -. A ~~ ~P A ) )
18	10 16 17	mpbir2an	|- A ~< ~P A