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 e. _V
Assertion canth
|- -. F : A -onto-> ~P A

Proof

Step Hyp Ref Expression
1 canth.1
 |-  A e. _V
2 ssrab2
 |-  { x e. A | -. x e. ( F ` x ) } C_ A
3 1 2 elpwi2
 |-  { x e. A | -. x e. ( F ` x ) } e. ~P A
4 forn
 |-  ( F : A -onto-> ~P A -> ran F = ~P A )
5 3 4 eleqtrrid
 |-  ( F : A -onto-> ~P A -> { x e. A | -. x e. ( F ` x ) } e. ran F )
6 id
 |-  ( x = y -> x = y )
7 fveq2
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
8 6 7 eleq12d
 |-  ( x = y -> ( x e. ( F ` x ) <-> y e. ( F ` y ) ) )
9 8 notbid
 |-  ( x = y -> ( -. x e. ( F ` x ) <-> -. y e. ( F ` y ) ) )
10 9 elrab
 |-  ( y e. { x e. A | -. x e. ( F ` x ) } <-> ( y e. A /\ -. y e. ( F ` y ) ) )
11 10 baibr
 |-  ( y e. A -> ( -. y e. ( F ` y ) <-> y e. { x e. A | -. x e. ( F ` x ) } ) )
12 nbbn
 |-  ( ( -. y e. ( F ` y ) <-> y e. { x e. A | -. x e. ( F ` x ) } ) <-> -. ( y e. ( F ` y ) <-> y e. { x e. A | -. x e. ( F ` x ) } ) )
13 11 12 sylib
 |-  ( y e. A -> -. ( y e. ( F ` y ) <-> y e. { x e. A | -. x e. ( F ` x ) } ) )
14 eleq2
 |-  ( ( F ` y ) = { x e. A | -. x e. ( F ` x ) } -> ( y e. ( F ` y ) <-> y e. { x e. A | -. x e. ( F ` x ) } ) )
15 13 14 nsyl
 |-  ( y e. A -> -. ( F ` y ) = { x e. A | -. x e. ( F ` x ) } )
16 15 nrex
 |-  -. E. y e. A ( F ` y ) = { x e. A | -. x e. ( F ` x ) }
17 fofn
 |-  ( F : A -onto-> ~P A -> F Fn A )
18 fvelrnb
 |-  ( F Fn A -> ( { x e. A | -. x e. ( F ` x ) } e. ran F <-> E. y e. A ( F ` y ) = { x e. A | -. x e. ( F ` x ) } ) )
19 17 18 syl
 |-  ( F : A -onto-> ~P A -> ( { x e. A | -. x e. ( F ` x ) } e. ran F <-> E. y e. A ( F ` y ) = { x e. A | -. x e. ( F ` x ) } ) )
20 16 19 mtbiri
 |-  ( F : A -onto-> ~P A -> -. { x e. A | -. x e. ( F ` x ) } e. ran F )
21 5 20 pm2.65i
 |-  -. F : A -onto-> ~P A