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