Metamath Proof Explorer

Theorem brwdomn0

Description: Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion brwdomn0 
|- ( X =/= (/) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )

Proof

Step Hyp Ref Expression
1 relwdom 
 |-  Rel ~<_*
2 1 brrelex2i 
 |-  ( X ~<_* Y -> Y e. _V )
3 2 a1i 
 |-  ( X =/= (/) -> ( X ~<_* Y -> Y e. _V ) )
4 fof 
 |-  ( z : Y -onto-> X -> z : Y --> X )
5 4 fdmd 
 |-  ( z : Y -onto-> X -> dom z = Y )
6 vex 
 |-  z e. _V
7 6 dmex 
 |-  dom z e. _V
8 5 7 eqeltrrdi 
 |-  ( z : Y -onto-> X -> Y e. _V )
9 8 exlimiv 
 |-  ( E. z z : Y -onto-> X -> Y e. _V )
10 9 a1i 
 |-  ( X =/= (/) -> ( E. z z : Y -onto-> X -> Y e. _V ) )
11 brwdom 
 |-  ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
12 df-ne 
 |-  ( X =/= (/) <-> -. X = (/) )
13 biorf 
 |-  ( -. X = (/) -> ( E. z z : Y -onto-> X <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
14 12 13 sylbi 
 |-  ( X =/= (/) -> ( E. z z : Y -onto-> X <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
15 14 bicomd 
 |-  ( X =/= (/) -> ( ( X = (/) \/ E. z z : Y -onto-> X ) <-> E. z z : Y -onto-> X ) )
16 11 15 sylan9bbr 
 |-  ( ( X =/= (/) /\ Y e. _V ) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )
17 16 ex 
 |-  ( X =/= (/) -> ( Y e. _V -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) ) )
18 3 10 17 pm5.21ndd 
 |-  ( X =/= (/) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )