Metamath Proof Explorer

Theorem wdomtr

Description: Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion wdomtr 
|- ( ( X ~<_* Y /\ Y ~<_* Z ) -> X ~<_* Z )

Proof

Step Hyp Ref Expression
1 relwdom 
 |-  Rel ~<_*
2 1 brrelex2i 
 |-  ( Y ~<_* Z -> Z e. _V )
3 2 adantl 
 |-  ( ( X ~<_* Y /\ Y ~<_* Z ) -> Z e. _V )
4 0wdom 
 |-  ( Z e. _V -> (/) ~<_* Z )
5 breq1 
 |-  ( X = (/) -> ( X ~<_* Z <-> (/) ~<_* Z ) )
6 4 5 syl5ibrcom 
 |-  ( Z e. _V -> ( X = (/) -> X ~<_* Z ) )
7 3 6 syl 
 |-  ( ( X ~<_* Y /\ Y ~<_* Z ) -> ( X = (/) -> X ~<_* Z ) )
8 simpll 
 |-  ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) -> X ~<_* Y )
9 brwdomn0 
 |-  ( X =/= (/) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )
10 9 adantl 
 |-  ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )
11 8 10 mpbid 
 |-  ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) -> E. z z : Y -onto-> X )
12 simpllr 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> Y ~<_* Z )
13 simplr 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> X =/= (/) )
14 dm0rn0 
 |-  ( dom z = (/) <-> ran z = (/) )
15 14 necon3bii 
 |-  ( dom z =/= (/) <-> ran z =/= (/) )
16 15 a1i 
 |-  ( z : Y -onto-> X -> ( dom z =/= (/) <-> ran z =/= (/) ) )
17 fof 
 |-  ( z : Y -onto-> X -> z : Y --> X )
18 17 fdmd 
 |-  ( z : Y -onto-> X -> dom z = Y )
19 18 neeq1d 
 |-  ( z : Y -onto-> X -> ( dom z =/= (/) <-> Y =/= (/) ) )
20 forn 
 |-  ( z : Y -onto-> X -> ran z = X )
21 20 neeq1d 
 |-  ( z : Y -onto-> X -> ( ran z =/= (/) <-> X =/= (/) ) )
22 16 19 21 3bitr3rd 
 |-  ( z : Y -onto-> X -> ( X =/= (/) <-> Y =/= (/) ) )
23 22 adantl 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> ( X =/= (/) <-> Y =/= (/) ) )
24 13 23 mpbid 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> Y =/= (/) )
25 brwdomn0 
 |-  ( Y =/= (/) -> ( Y ~<_* Z <-> E. y y : Z -onto-> Y ) )
26 24 25 syl 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> ( Y ~<_* Z <-> E. y y : Z -onto-> Y ) )
27 12 26 mpbid 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> E. y y : Z -onto-> Y )
28 vex 
 |-  z e. _V
29 vex 
 |-  y e. _V
30 28 29 coex 
 |-  ( z o. y ) e. _V
31 foco 
 |-  ( ( z : Y -onto-> X /\ y : Z -onto-> Y ) -> ( z o. y ) : Z -onto-> X )
32 fowdom 
 |-  ( ( ( z o. y ) e. _V /\ ( z o. y ) : Z -onto-> X ) -> X ~<_* Z )
33 30 31 32 sylancr 
 |-  ( ( z : Y -onto-> X /\ y : Z -onto-> Y ) -> X ~<_* Z )
34 33 adantl 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ ( z : Y -onto-> X /\ y : Z -onto-> Y ) ) -> X ~<_* Z )
35 34 expr 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> ( y : Z -onto-> Y -> X ~<_* Z ) )
36 35 exlimdv 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> ( E. y y : Z -onto-> Y -> X ~<_* Z ) )
37 27 36 mpd 
 |-  ( ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) /\ z : Y -onto-> X ) -> X ~<_* Z )
38 11 37 exlimddv 
 |-  ( ( ( X ~<_* Y /\ Y ~<_* Z ) /\ X =/= (/) ) -> X ~<_* Z )
39 38 ex 
 |-  ( ( X ~<_* Y /\ Y ~<_* Z ) -> ( X =/= (/) -> X ~<_* Z ) )
40 7 39 pm2.61dne 
 |-  ( ( X ~<_* Y /\ Y ~<_* Z ) -> X ~<_* Z )