This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 undif2 
 |-  ( A u. ( C \ A ) ) = ( A u. C )
2 reldom 
 |-  Rel ~<_
3 2 brrelex2i 
 |-  ( A ~<_ B -> B e. _V )
4 2 brrelex2i 
 |-  ( C ~<_ D -> D e. _V )
5 unexg 
 |-  ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
6 3 4 5 syl2an 
 |-  ( ( A ~<_ B /\ C ~<_ D ) -> ( B u. D ) e. _V )
7 6 adantr 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( B u. D ) e. _V )
8 brdomi 
 |-  ( A ~<_ B -> E. x x : A -1-1-> B )
9 brdomi 
 |-  ( C ~<_ D -> E. y y : C -1-1-> D )
10 exdistrv 
 |-  ( E. x E. y ( x : A -1-1-> B /\ y : C -1-1-> D ) <-> ( E. x x : A -1-1-> B /\ E. y y : C -1-1-> D ) )
11 disjdif 
 |-  ( A i^i ( C \ A ) ) = (/)
12 difss 
 |-  ( C \ A ) C_ C
13 f1ssres 
 |-  ( ( y : C -1-1-> D /\ ( C \ A ) C_ C ) -> ( y |` ( C \ A ) ) : ( C \ A ) -1-1-> D )
14 12 13 mpan2 
 |-  ( y : C -1-1-> D -> ( y |` ( C \ A ) ) : ( C \ A ) -1-1-> D )
15 f1un 
 |-  ( ( ( x : A -1-1-> B /\ ( y |` ( C \ A ) ) : ( C \ A ) -1-1-> D ) /\ ( ( A i^i ( C \ A ) ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) )
16 14 15 sylanl2 
 |-  ( ( ( x : A -1-1-> B /\ y : C -1-1-> D ) /\ ( ( A i^i ( C \ A ) ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) )
17 11 16 mpanr1 
 |-  ( ( ( x : A -1-1-> B /\ y : C -1-1-> D ) /\ ( B i^i D ) = (/) ) -> ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) )
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 19 resex 
 |-  ( y |` ( C \ A ) ) e. _V
21 18 20 unex 
 |-  ( x u. ( y |` ( C \ A ) ) ) e. _V
22 f1dom3g 
 |-  ( ( ( x u. ( y |` ( C \ A ) ) ) e. _V /\ ( B u. D ) e. _V /\ ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) ) -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) )
23 21 22 mp3an1 
 |-  ( ( ( B u. D ) e. _V /\ ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) ) -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) )
24 23 expcom 
 |-  ( ( x u. ( y |` ( C \ A ) ) ) : ( A u. ( C \ A ) ) -1-1-> ( B u. D ) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) )
25 17 24 syl 
 |-  ( ( ( x : A -1-1-> B /\ y : C -1-1-> D ) /\ ( B i^i D ) = (/) ) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) )
26 25 ex 
 |-  ( ( x : A -1-1-> B /\ y : C -1-1-> D ) -> ( ( B i^i D ) = (/) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) ) )
27 26 exlimivv 
 |-  ( E. x E. y ( x : A -1-1-> B /\ y : C -1-1-> D ) -> ( ( B i^i D ) = (/) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) ) )
28 10 27 sylbir 
 |-  ( ( E. x x : A -1-1-> B /\ E. y y : C -1-1-> D ) -> ( ( B i^i D ) = (/) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) ) )
29 8 9 28 syl2an 
 |-  ( ( A ~<_ B /\ C ~<_ D ) -> ( ( B i^i D ) = (/) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) ) )
30 29 imp 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( ( B u. D ) e. _V -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) ) )
31 7 30 mpd 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( A u. ( C \ A ) ) ~<_ ( B u. D ) )
32 1 31 eqbrtrrid 
 |-  ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~<_ ( B u. D ) )