Metamath Proof Explorer


Theorem canth

Description: No set A is equinumerous to its power set (Cantor's theorem), i.e., no function can map A onto its power set. Compare Theorem 6B(b) of Enderton p. 132. For the equinumerosity version, see canth2 . Note that A must be a set: this theorem does not hold when A is too large to be a set; see ncanth for a counterexample. (Use nex if you want the form -. E. f f : A -onto-> ~P A .) (Contributed by NM, 7-Aug-1994) (Proof shortened by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypothesis canth.1 A V
Assertion canth ¬ F : A onto 𝒫 A

Proof

Step Hyp Ref Expression
1 canth.1 A V
2 ssrab2 x A | ¬ x F x A
3 1 2 elpwi2 x A | ¬ x F x 𝒫 A
4 forn F : A onto 𝒫 A ran F = 𝒫 A
5 3 4 eleqtrrid F : A onto 𝒫 A x A | ¬ x F x ran F
6 id x = y x = y
7 fveq2 x = y F x = F y
8 6 7 eleq12d x = y x F x y F y
9 8 notbid x = y ¬ x F x ¬ y F y
10 9 elrab y x A | ¬ x F x y A ¬ y F y
11 10 baibr y A ¬ y F y y x A | ¬ x F x
12 nbbn ¬ y F y y x A | ¬ x F x ¬ y F y y x A | ¬ x F x
13 11 12 sylib y A ¬ y F y y x A | ¬ x F x
14 eleq2 F y = x A | ¬ x F x y F y y x A | ¬ x F x
15 13 14 nsyl y A ¬ F y = x A | ¬ x F x
16 15 nrex ¬ y A F y = x A | ¬ x F x
17 fofn F : A onto 𝒫 A F Fn A
18 fvelrnb F Fn A x A | ¬ x F x ran F y A F y = x A | ¬ x F x
19 17 18 syl F : A onto 𝒫 A x A | ¬ x F x ran F y A F y = x A | ¬ x F x
20 16 19 mtbiri F : A onto 𝒫 A ¬ x A | ¬ x F x ran F
21 5 20 pm2.65i ¬ F : A onto 𝒫 A