Metamath Proof Explorer

Theorem enssdom

Description: Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion enssdom 
|- ~~ C_ ~<_

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 f1of1 
 |-  ( f : x -1-1-onto-> y -> f : x -1-1-> y )
3 2 eximi 
 |-  ( E. f f : x -1-1-onto-> y -> E. f f : x -1-1-> y )
4 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | E. f f : x -1-1-onto-> y } <-> E. f f : x -1-1-onto-> y )
5 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | E. f f : x -1-1-> y } <-> E. f f : x -1-1-> y )
6 3 4 5 3imtr4i 
 |-  ( <. x , y >. e. { <. x , y >. | E. f f : x -1-1-onto-> y } -> <. x , y >. e. { <. x , y >. | E. f f : x -1-1-> y } )
7 df-en 
 |-  ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
8 7 eleq2i 
 |-  ( <. x , y >. e. ~~ <-> <. x , y >. e. { <. x , y >. | E. f f : x -1-1-onto-> y } )
9 df-dom 
 |-  ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
10 9 eleq2i 
 |-  ( <. x , y >. e. ~<_ <-> <. x , y >. e. { <. x , y >. | E. f f : x -1-1-> y } )
11 6 8 10 3imtr4i 
 |-  ( <. x , y >. e. ~~ -> <. x , y >. e. ~<_ )
12 1 11 relssi 
 |-  ~~ C_ ~<_