Metamath Proof Explorer

Theorem brwdom

Description: Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( Y e. V -> Y e. _V )
2 relwdom 
 |-  Rel ~<_*
3 2 brrelex1i 
 |-  ( X ~<_* Y -> X e. _V )
4 3 a1i 
 |-  ( Y e. _V -> ( X ~<_* Y -> X e. _V ) )
5 0ex 
 |-  (/) e. _V
6 eleq1a 
 |-  ( (/) e. _V -> ( X = (/) -> X e. _V ) )
7 5 6 ax-mp 
 |-  ( X = (/) -> X e. _V )
8 forn 
 |-  ( z : Y -onto-> X -> ran z = X )
9 vex 
 |-  z e. _V
10 9 rnex 
 |-  ran z e. _V
11 8 10 eqeltrrdi 
 |-  ( z : Y -onto-> X -> X e. _V )
12 11 exlimiv 
 |-  ( E. z z : Y -onto-> X -> X e. _V )
13 7 12 jaoi 
 |-  ( ( X = (/) \/ E. z z : Y -onto-> X ) -> X e. _V )
14 13 a1i 
 |-  ( Y e. _V -> ( ( X = (/) \/ E. z z : Y -onto-> X ) -> X e. _V ) )
15 eqeq1 
 |-  ( x = X -> ( x = (/) <-> X = (/) ) )
16 foeq3 
 |-  ( x = X -> ( z : y -onto-> x <-> z : y -onto-> X ) )
17 16 exbidv 
 |-  ( x = X -> ( E. z z : y -onto-> x <-> E. z z : y -onto-> X ) )
18 15 17 orbi12d 
 |-  ( x = X -> ( ( x = (/) \/ E. z z : y -onto-> x ) <-> ( X = (/) \/ E. z z : y -onto-> X ) ) )
19 foeq2 
 |-  ( y = Y -> ( z : y -onto-> X <-> z : Y -onto-> X ) )
20 19 exbidv 
 |-  ( y = Y -> ( E. z z : y -onto-> X <-> E. z z : Y -onto-> X ) )
21 20 orbi2d 
 |-  ( y = Y -> ( ( X = (/) \/ E. z z : y -onto-> X ) <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
22 df-wdom 
 |-  ~<_* = { <. x , y >. | ( x = (/) \/ E. z z : y -onto-> x ) }
23 18 21 22 brabg 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
24 23 expcom 
 |-  ( Y e. _V -> ( X e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) ) )
25 4 14 24 pm5.21ndd 
 |-  ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
26 1 25 syl 
 |-  ( Y e. V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )