Metamath Proof Explorer

Theorem enssdom

Description: Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998) (Proof shortened by TM, 10-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 f1of1 
 |-  ( f : x -1-1-onto-> y -> f : x -1-1-> y )
2 1 eximi 
 |-  ( E. f f : x -1-1-onto-> y -> E. f f : x -1-1-> y )
3 2 ssopab2i 
 |-  { <. x , y >. | E. f f : x -1-1-onto-> y } C_ { <. x , y >. | E. f f : x -1-1-> y }
4 df-en 
 |-  ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
5 df-dom 
 |-  ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
6 3 4 5 3sstr4i 
 |-  ~~ C_ ~<_