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

Metamath Proof Explorer

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