Theorem canthwdom

Description: Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 , equivalent to canth ). (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	canthwdom	|- -. ~P A ~<_* A

Proof

Step	Hyp	Ref	Expression
1		0elpw	|- (/) e. ~P A
2		ne0i	|- ( (/) e. ~P A -> ~P A =/= (/) )
3	1 2	mp1i	|- ( ~P A ~<_* A -> ~P A =/= (/) )
4		brwdomn0	|- ( ~P A =/= (/) -> ( ~P A ~<_* A <-> E. f f : A -onto-> ~P A ) )
5	3 4	syl	|- ( ~P A ~<_* A -> ( ~P A ~<_* A <-> E. f f : A -onto-> ~P A ) )
6	5	ibi	|- ( ~P A ~<_* A -> E. f f : A -onto-> ~P A )
7		relwdom	|- Rel ~<_*
8	7	brrelex2i	|- ( ~P A ~<_* A -> A e. _V )
9		foeq2	|- ( x = A -> ( f : x -onto-> ~P x <-> f : A -onto-> ~P x ) )
10		pweq	|- ( x = A -> ~P x = ~P A )
11		foeq3	|- ( ~P x = ~P A -> ( f : A -onto-> ~P x <-> f : A -onto-> ~P A ) )
12	10 11	syl	|- ( x = A -> ( f : A -onto-> ~P x <-> f : A -onto-> ~P A ) )
13	9 12	bitrd	|- ( x = A -> ( f : x -onto-> ~P x <-> f : A -onto-> ~P A ) )
14	13	notbid	|- ( x = A -> ( -. f : x -onto-> ~P x <-> -. f : A -onto-> ~P A ) )
15		vex	|- x e. _V
16	15	canth	|- -. f : x -onto-> ~P x
17	14 16	vtoclg	|- ( A e. _V -> -. f : A -onto-> ~P A )
18	8 17	syl	|- ( ~P A ~<_* A -> -. f : A -onto-> ~P A )
19	18	nexdv	|- ( ~P A ~<_* A -> -. E. f f : A -onto-> ~P A )
20	6 19	pm2.65i	|- -. ~P A ~<_* A