Theorem undom 7155

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.)

Assertion

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

Proof of Theorem undom

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 7074	. . . . . . 7 |- Rel ~<_
2	1	brrelex2i 4878	. . . . . 6 |- ( A ~<_ B -> B e. _V )
3		domeng 7081	. . . . . 6 |- ( B e. _V -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
4	2, 3	syl 16	. . . . 5 |- ( A ~<_ B -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) )
5	4	ibi 233	. . . 4 |- ( A ~<_ B -> E. x ( A ~~ x /\ x C_ B ) )
6	1	brrelexi 4877	. . . . . . 7 |- ( C ~<_ D -> C e. _V )
7		difss 3434	. . . . . . 7 |- ( C \ A ) C_ C
8		ssdomg 7112	. . . . . . 7 |- ( C e. _V -> ( ( C \ A ) C_ C -> ( C \ A ) ~<_ C ) )
9	6, 7, 8	ee10 1382	. . . . . 6 |- ( C ~<_ D -> ( C \ A ) ~<_ C )
10		domtr 7119	. . . . . 6 |- ( ( ( C \ A ) ~<_ C /\ C ~<_ D ) -> ( C \ A ) ~<_ D )
11	9, 10	mpancom 651	. . . . 5 |- ( C ~<_ D -> ( C \ A ) ~<_ D )
12	1	brrelex2i 4878	. . . . . . 7 |- ( ( C \ A ) ~<_ D -> D e. _V )
13		domeng 7081	. . . . . . 7 |- ( D e. _V -> ( ( C \ A ) ~<_ D <-> E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
14	12, 13	syl 16	. . . . . 6 |- ( ( C \ A ) ~<_ D -> ( ( C \ A ) ~<_ D <-> E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
15	14	ibi 233	. . . . 5 |- ( ( C \ A ) ~<_ D -> E. y ( ( C \ A ) ~~ y /\ y C_ D ) )
16	11, 15	syl 16	. . . 4 |- ( C ~<_ D -> E. y ( ( C \ A ) ~~ y /\ y C_ D ) )
17	5, 16	anim12i 550	. . 3 |- ( ( A ~<_ B /\ C ~<_ D ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
18	17	adantr 452	. 2 |- ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
19		eeanv 1933	. . 3 |- ( 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 739	. . . . . . 7 |- ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> A ~~ x )
21		simprrl 741	. . . . . . 7 |- ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> ( C \ A ) ~~ y )
22		disjdif 3660	. . . . . . . 8 |- ( A i^i ( C \ A ) ) = (/)
23	22	a1i 11	. . . . . . 7 |- ( ( ( ( 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 3528	. . . . . . . . . 10 |- ( ( x C_ B /\ y C_ D ) -> ( x i^i y ) C_ ( B i^i D ) )
25	24	ad2ant2l 727	. . . . . . . . 9 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x i^i y ) C_ ( B i^i D ) )
26	25	adantl 453	. . . . . . . 8 |- ( ( ( ( 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 732	. . . . . . . 8 |- ( ( ( ( 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 3619	. . . . . . . 8 |- ( ( ( x i^i y ) C_ ( B i^i D ) /\ ( B i^i D ) = (/) ) -> ( x i^i y ) = (/) )
29	26, 27, 28	syl2anc 643	. . . . . . 7 |- ( ( ( ( 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 3664	. . . . . . . 8 |- ( A u. ( C \ A ) ) = ( A u. C )
31		unen 7148	. . . . . . . 8 |- ( ( ( A ~~ x /\ ( C \ A ) ~~ y ) /\ ( ( A i^i ( C \ A ) ) = (/) /\ ( x i^i y ) = (/) ) ) -> ( A u. ( C \ A ) ) ~~ ( x u. y ) )
32	30, 31	syl5eqbrr 4206	. . . . . . 7 |- ( ( ( 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 1185	. . . . . 6 |- ( ( ( ( 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 711	. . . . . . . 8 |- ( ( ( ( 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 4878	. . . . . . . . 9 |- ( C ~<_ D -> D e. _V )
36	35	ad3antlr 712	. . . . . . . 8 |- ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> D e. _V )
37		unexg 4669	. . . . . . . 8 |- ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
38	34, 36, 37	syl2anc 643	. . . . . . 7 |- ( ( ( ( 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 3479	. . . . . . . . 9 |- ( ( x C_ B /\ y C_ D ) -> ( x u. y ) C_ ( B u. D ) )
40	39	ad2ant2l 727	. . . . . . . 8 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x u. y ) C_ ( B u. D ) )
41	40	adantl 453	. . . . . . 7 |- ( ( ( ( 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 7112	. . . . . . 7 |- ( ( B u. D ) e. _V -> ( ( x u. y ) C_ ( B u. D ) -> ( x u. y ) ~<_ ( B u. D ) ) )
43	38, 41, 42	sylc 58	. . . . . 6 |- ( ( ( ( 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 7124	. . . . . 6 |- ( ( ( A u. C ) ~~ ( x u. y ) /\ ( x u. y ) ~<_ ( B u. D ) ) -> ( A u. C ) ~<_ ( B u. D ) )
45	33, 43, 44	syl2anc 643	. . . . 5 |- ( ( ( ( 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 424	. . . 4 |- ( ( ( 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 1644	. . 3 |- ( ( ( 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 210	. 2 |- ( ( ( 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 15	1 |- ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) -> ( A u. C ) ~<_ ( B u. D ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   E.wex 1547   = wceq 1649   e. wcel 1721   _Vcvv 2916   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   class class class wbr 4172   ~~ cen 7065   ~<_ cdom 7066

This theorem is referenced by:  domunsncan  7167  domunsn  7216  sucdom2  7262  unxpdom2  7276  sucxpdom  7277  fodomfi  7344  uncdadom  8007  cdadom1  8022

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-en 7069  df-dom 7070