Metamath Proof Explorer


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 V
Assertion canth2 A 𝒫 A

Proof

Step Hyp Ref Expression
1 canth2.1 A V
2 1 pwex 𝒫 A V
3 snelpwi x A x 𝒫 A
4 vex x 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 A y A x = y x = y
9 3 8 dom3 A V 𝒫 A V A 𝒫 A
10 1 2 9 mp2an A 𝒫 A
11 1 canth ¬ f : A onto 𝒫 A
12 f1ofo f : A 1-1 onto 𝒫 A f : A onto 𝒫 A
13 11 12 mto ¬ f : A 1-1 onto 𝒫 A
14 13 nex ¬ f f : A 1-1 onto 𝒫 A
15 bren A 𝒫 A f f : A 1-1 onto 𝒫 A
16 14 15 mtbir ¬ A 𝒫 A
17 brsdom A 𝒫 A A 𝒫 A ¬ A 𝒫 A
18 10 16 17 mpbir2an A 𝒫 A