Metamath Proof Explorer

Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998) (Proof shortened by BTernaryTau, 29-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 brdom2g 
 |-  ( ( A e. _V /\ B e. C ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
2 1 ex 
 |-  ( A e. _V -> ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) )
3 reldom 
 |-  Rel ~<_
4 3 brrelex1i 
 |-  ( A ~<_ B -> A e. _V )
5 f1f 
 |-  ( f : A -1-1-> B -> f : A --> B )
6 fdm 
 |-  ( f : A --> B -> dom f = A )
7 vex 
 |-  f e. _V
8 7 dmex 
 |-  dom f e. _V
9 6 8 eqeltrrdi 
 |-  ( f : A --> B -> A e. _V )
10 5 9 syl 
 |-  ( f : A -1-1-> B -> A e. _V )
11 10 exlimiv 
 |-  ( E. f f : A -1-1-> B -> A e. _V )
12 4 11 pm5.21ni 
 |-  ( -. A e. _V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
13 12 a1d 
 |-  ( -. A e. _V -> ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) ) )
14 2 13 pm2.61i 
 |-  ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )