Metamath Proof Explorer

Theorem brdomi

Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015) Avoid ax-un . (Revised by BTernaryTau, 29-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex12i 
 |-  ( A ~<_ B -> ( A e. _V /\ B e. _V ) )
3 brdom2g 
 |-  ( ( A e. _V /\ 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 )