Metamath Proof Explorer

Theorem unwdomg

Description: Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion unwdomg 
|- ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~<_* ( B u. D ) )

Proof

Step Hyp Ref Expression
1 brwdom3i 
 |-  ( A ~<_* B -> E. f A. a e. A E. b e. B a = ( f ` b ) )
2 1 3ad2ant1 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> E. f A. a e. A E. b e. B a = ( f ` b ) )
3 brwdom3i 
 |-  ( C ~<_* D -> E. g A. a e. C E. b e. D a = ( g ` b ) )
4 3 3ad2ant2 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> E. g A. a e. C E. b e. D a = ( g ` b ) )
5 4 adantr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> E. g A. a e. C E. b e. D a = ( g ` b ) )
6 relwdom 
 |-  Rel ~<_*
7 6 brrelex1i 
 |-  ( A ~<_* B -> A e. _V )
8 6 brrelex1i 
 |-  ( C ~<_* D -> C e. _V )
9 unexg 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A u. C ) e. _V )
10 7 8 9 syl2an 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( A u. C ) e. _V )
11 10 3adant3 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> ( A u. C ) e. _V )
12 11 adantr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) -> ( A u. C ) e. _V )
13 6 brrelex2i 
 |-  ( A ~<_* B -> B e. _V )
14 6 brrelex2i 
 |-  ( C ~<_* D -> D e. _V )
15 unexg 
 |-  ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
16 13 14 15 syl2an 
 |-  ( ( A ~<_* B /\ C ~<_* D ) -> ( B u. D ) e. _V )
17 16 3adant3 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> ( B u. D ) e. _V )
18 17 adantr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) -> ( B u. D ) e. _V )
19 elun 
 |-  ( y e. ( A u. C ) <-> ( y e. A \/ y e. C ) )
20 eqeq1 
 |-  ( a = y -> ( a = ( f ` b ) <-> y = ( f ` b ) ) )
21 20 rexbidv 
 |-  ( a = y -> ( E. b e. B a = ( f ` b ) <-> E. b e. B y = ( f ` b ) ) )
22 21 rspcva 
 |-  ( ( y e. A /\ A. a e. A E. b e. B a = ( f ` b ) ) -> E. b e. B y = ( f ` b ) )
23 fveq2 
 |-  ( b = z -> ( f ` b ) = ( f ` z ) )
24 23 eqeq2d 
 |-  ( b = z -> ( y = ( f ` b ) <-> y = ( f ` z ) ) )
25 24 cbvrexvw 
 |-  ( E. b e. B y = ( f ` b ) <-> E. z e. B y = ( f ` z ) )
26 ssun1 
 |-  B C_ ( B u. D )
27 iftrue 
 |-  ( z e. B -> if ( z e. B , f , g ) = f )
28 27 fveq1d 
 |-  ( z e. B -> ( if ( z e. B , f , g ) ` z ) = ( f ` z ) )
29 28 eqeq2d 
 |-  ( z e. B -> ( y = ( if ( z e. B , f , g ) ` z ) <-> y = ( f ` z ) ) )
30 29 biimprd 
 |-  ( z e. B -> ( y = ( f ` z ) -> y = ( if ( z e. B , f , g ) ` z ) ) )
31 30 reximia 
 |-  ( E. z e. B y = ( f ` z ) -> E. z e. B y = ( if ( z e. B , f , g ) ` z ) )
32 ssrexv 
 |-  ( B C_ ( B u. D ) -> ( E. z e. B y = ( if ( z e. B , f , g ) ` z ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) ) )
33 26 31 32 mpsyl 
 |-  ( E. z e. B y = ( f ` z ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
34 25 33 sylbi 
 |-  ( E. b e. B y = ( f ` b ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
35 22 34 syl 
 |-  ( ( y e. A /\ A. a e. A E. b e. B a = ( f ` b ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
36 35 ancoms 
 |-  ( ( A. a e. A E. b e. B a = ( f ` b ) /\ y e. A ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
37 36 adantlr 
 |-  ( ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) /\ y e. A ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
38 37 adantll 
 |-  ( ( ( ( B i^i D ) = (/) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) /\ y e. A ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
39 eqeq1 
 |-  ( a = y -> ( a = ( g ` b ) <-> y = ( g ` b ) ) )
40 39 rexbidv 
 |-  ( a = y -> ( E. b e. D a = ( g ` b ) <-> E. b e. D y = ( g ` b ) ) )
41 fveq2 
 |-  ( b = z -> ( g ` b ) = ( g ` z ) )
42 41 eqeq2d 
 |-  ( b = z -> ( y = ( g ` b ) <-> y = ( g ` z ) ) )
43 42 cbvrexvw 
 |-  ( E. b e. D y = ( g ` b ) <-> E. z e. D y = ( g ` z ) )
44 40 43 bitrdi 
 |-  ( a = y -> ( E. b e. D a = ( g ` b ) <-> E. z e. D y = ( g ` z ) ) )
45 44 rspccva 
 |-  ( ( A. a e. C E. b e. D a = ( g ` b ) /\ y e. C ) -> E. z e. D y = ( g ` z ) )
46 ssun2 
 |-  D C_ ( B u. D )
47 minel 
 |-  ( ( z e. D /\ ( B i^i D ) = (/) ) -> -. z e. B )
48 47 ancoms 
 |-  ( ( ( B i^i D ) = (/) /\ z e. D ) -> -. z e. B )
49 48 iffalsed 
 |-  ( ( ( B i^i D ) = (/) /\ z e. D ) -> if ( z e. B , f , g ) = g )
50 49 fveq1d 
 |-  ( ( ( B i^i D ) = (/) /\ z e. D ) -> ( if ( z e. B , f , g ) ` z ) = ( g ` z ) )
51 50 eqeq2d 
 |-  ( ( ( B i^i D ) = (/) /\ z e. D ) -> ( y = ( if ( z e. B , f , g ) ` z ) <-> y = ( g ` z ) ) )
52 51 biimprd 
 |-  ( ( ( B i^i D ) = (/) /\ z e. D ) -> ( y = ( g ` z ) -> y = ( if ( z e. B , f , g ) ` z ) ) )
53 52 reximdva 
 |-  ( ( B i^i D ) = (/) -> ( E. z e. D y = ( g ` z ) -> E. z e. D y = ( if ( z e. B , f , g ) ` z ) ) )
54 53 imp 
 |-  ( ( ( B i^i D ) = (/) /\ E. z e. D y = ( g ` z ) ) -> E. z e. D y = ( if ( z e. B , f , g ) ` z ) )
55 ssrexv 
 |-  ( D C_ ( B u. D ) -> ( E. z e. D y = ( if ( z e. B , f , g ) ` z ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) ) )
56 46 54 55 mpsyl 
 |-  ( ( ( B i^i D ) = (/) /\ E. z e. D y = ( g ` z ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
57 45 56 sylan2 
 |-  ( ( ( B i^i D ) = (/) /\ ( A. a e. C E. b e. D a = ( g ` b ) /\ y e. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
58 57 anassrs 
 |-  ( ( ( ( B i^i D ) = (/) /\ A. a e. C E. b e. D a = ( g ` b ) ) /\ y e. C ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
59 58 adantlrl 
 |-  ( ( ( ( B i^i D ) = (/) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) /\ y e. C ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
60 38 59 jaodan 
 |-  ( ( ( ( B i^i D ) = (/) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) /\ ( y e. A \/ y e. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
61 19 60 sylan2b 
 |-  ( ( ( ( B i^i D ) = (/) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) /\ y e. ( A u. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
62 61 expl 
 |-  ( ( B i^i D ) = (/) -> ( ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) /\ y e. ( A u. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) ) )
63 62 3ad2ant3 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> ( ( ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) /\ y e. ( A u. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) ) )
64 63 impl 
 |-  ( ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) /\ y e. ( A u. C ) ) -> E. z e. ( B u. D ) y = ( if ( z e. B , f , g ) ` z ) )
65 12 18 64 wdom2d 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ ( A. a e. A E. b e. B a = ( f ` b ) /\ A. a e. C E. b e. D a = ( g ` b ) ) ) -> ( A u. C ) ~<_* ( B u. D ) )
66 65 expr 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> ( A. a e. C E. b e. D a = ( g ` b ) -> ( A u. C ) ~<_* ( B u. D ) ) )
67 66 exlimdv 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> ( E. g A. a e. C E. b e. D a = ( g ` b ) -> ( A u. C ) ~<_* ( B u. D ) ) )
68 5 67 mpd 
 |-  ( ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) /\ A. a e. A E. b e. B a = ( f ` b ) ) -> ( A u. C ) ~<_* ( B u. D ) )
69 2 68 exlimddv 
 |-  ( ( A ~<_* B /\ C ~<_* D /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~<_* ( B u. D ) )