Metamath Proof Explorer

Theorem undom

Description: Dominance law for union. Proposition 4.24(a) of Mendelson p. 257. (Contributed by NM, 3-Sep-2004) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
3 domeng 
 |-  ( B e. _V -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
4 2 3 syl 
 |-  ( A ~<_ B -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
5 4 ibi 
 |-  ( A ~<_ B -> E. x ( A ~~ x /\ x C_ B ) )
6 1 brrelex1i 
 |-  ( C ~<_ D -> C e. _V )
7 difss 
 |-  ( C \ A ) C_ C
8 ssdomg 
 |-  ( C e. _V -> ( ( C \ A ) C_ C -> ( C \ A ) ~<_ C ) )
9 6 7 8 mpisyl 
 |-  ( C ~<_ D -> ( C \ A ) ~<_ C )
10 domtr 
 |-  ( ( ( C \ A ) ~<_ C /\ C ~<_ D ) -> ( C \ A ) ~<_ D )
11 9 10 mpancom 
 |-  ( C ~<_ D -> ( C \ A ) ~<_ D )
12 1 brrelex2i 
 |-  ( ( C \ A ) ~<_ D -> D e. _V )
13 domeng 
 |-  ( D e. _V -> ( ( C \ A ) ~<_ D <-> E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
14 12 13 syl 
 |-  ( ( C \ A ) ~<_ D -> ( ( C \ A ) ~<_ D <-> E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
15 14 ibi 
 |-  ( ( C \ A ) ~<_ D -> E. y ( ( C \ A ) ~~ y /\ y C_ D ) )
16 11 15 syl 
 |-  ( C ~<_ D -> E. y ( ( C \ A ) ~~ y /\ y C_ D ) )
17 5 16 anim12i 
 |-  ( ( A ~<_ B /\ C ~<_ D ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
18 17 adantr 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
19 exdistrv 
 |-  ( E. x E. y ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) <-> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
20 simprll 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> A ~~ x )
21 simprrl 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( C \ A ) ~~ y )
22 disjdif 
 |-  ( A i^i ( C \ A ) ) = (/)
23 22 a1i 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( A i^i ( C \ A ) ) = (/) )
24 ss2in 
 |-  ( ( x C_ B /\ y C_ D ) -> ( x i^i y ) C_ ( B i^i D ) )
25 24 ad2ant2l 
 |-  ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x i^i y ) C_ ( B i^i D ) )
26 25 adantl 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( x i^i y ) C_ ( B i^i D ) )
27 simplr 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( B i^i D ) = (/) )
28 sseq0 
 |-  ( ( ( x i^i y ) C_ ( B i^i D ) /\ ( B i^i D ) = (/) ) -> ( x i^i y ) = (/) )
29 26 27 28 syl2anc 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( x i^i y ) = (/) )
30 undif2 
 |-  ( A u. ( C \ A ) ) = ( A u. C )
31 unen 
 |-  ( ( ( A ~~ x /\ ( C \ A ) ~~ y ) /\ ( ( A i^i ( C \ A ) ) = (/) /\ ( x i^i y ) = (/) ) ) -> ( A u. ( C \ A ) ) ~~ ( x u. y ) )
32 30 31 eqbrtrrid 
 |-  ( ( ( A ~~ x /\ ( C \ A ) ~~ y ) /\ ( ( A i^i ( C \ A ) ) = (/) /\ ( x i^i y ) = (/) ) ) -> ( A u. C ) ~~ ( x u. y ) )
33 20 21 23 29 32 syl22anc 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( A u. C ) ~~ ( x u. y ) )
34 2 ad3antrrr 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> B e. _V )
35 1 brrelex2i 
 |-  ( C ~<_ D -> D e. _V )
36 35 ad3antlr 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> D e. _V )
37 unexg 
 |-  ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
38 34 36 37 syl2anc 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( B u. D ) e. _V )
39 unss12 
 |-  ( ( x C_ B /\ y C_ D ) -> ( x u. y ) C_ ( B u. D ) )
40 39 ad2ant2l 
 |-  ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x u. y ) C_ ( B u. D ) )
41 40 adantl 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( x u. y ) C_ ( B u. D ) )
42 ssdomg 
 |-  ( ( B u. D ) e. _V -> ( ( x u. y ) C_ ( B u. D ) -> ( x u. y ) ~<_ ( B u. D ) ) )
43 38 41 42 sylc 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( x u. y ) ~<_ ( B u. D ) )
44 endomtr 
 |-  ( ( ( A u. C ) ~~ ( x u. y ) /\ ( x u. y ) ~<_ ( B u. D ) ) -> ( A u. C ) ~<_ ( B u. D ) )
45 33 43 44 syl2anc 
 |-  ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( A u. C ) ~<_ ( B u. D ) )
46 45 ex 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( A u. C ) ~<_ ( B u. D ) ) )
47 46 exlimdvv 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( E. x E. y ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( A u. C ) ~<_ ( B u. D ) ) )
48 19 47 syl5bir 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( A u. C ) ~<_ ( B u. D ) ) )
49 18 48 mpd 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~<_ ( B u. D ) )