Metamath Proof Explorer

Theorem brdomi

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion brdomi 
|- ( A ~<_ B -> E. f f : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
3 brdomg 
 |-  ( B e. _V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
4 2 3 syl 
 |-  ( A ~<_ B -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
5 4 ibi 
 |-  ( A ~<_ B -> E. f f : A -1-1-> B )