This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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