Theorem undom 7391

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 7308	. . . . . . 7 |- Rel ~<_
2	1	brrelex2i 4875	. . . . . 6 |- ( A ~<_ B -> B e. _V )
3		domeng 7316	. . . . . 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 241	. . . 4 |- ( A ~<_ B -> E. x ( A ~~ x /\ x C_ B ) )
6	1	brrelexi 4874	. . . . . . 7 |- ( C ~<_ D -> C e. _V )
7		difss 3478	. . . . . . 7 |- ( C \ A ) C_ C
8		ssdomg 7347	. . . . . . 7 |- ( C e. _V -> ( ( C \ A ) C_ C -> ( C \ A ) ~<_ C ) )
9	6, 7, 8	mpisyl 18	. . . . . 6 |- ( C ~<_ D -> ( C \ A ) ~<_ C )
10		domtr 7354	. . . . . 6 |- ( ( ( C \ A ) ~<_ C /\ C ~<_ D ) -> ( C \ A ) ~<_ D )
11	9, 10	mpancom 669	. . . . 5 |- ( C ~<_ D -> ( C \ A ) ~<_ D )
12	1	brrelex2i 4875	. . . . . . 7 |- ( ( C \ A ) ~<_ D -> D e. _V )
13		domeng 7316	. . . . . . 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 241	. . . . 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 566	. . 3 |- ( ( A ~<_ B /\ C ~<_ D ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
18	17	adantr 465	. 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 1931	. . 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 761	. . . . . . 7 |- ( ( ( ( A ~<_ B /\ C ~<_ D ) /\ ( B i^i D ) = (/) ) /\ ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) ) -> A ~~ x )
21		simprrl 763	. . . . . . 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 3746	. . . . . . . 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 3572	. . . . . . . . . 10 |- ( ( x C_ B /\ y C_ D ) -> ( x i^i y ) C_ ( B i^i D ) )
25	24	ad2ant2l 745	. . . . . . . . 9 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x i^i y ) C_ ( B i^i D ) )
26	25	adantl 466	. . . . . . . 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 754	. . . . . . . 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 3664	. . . . . . . 8 |- ( ( ( x i^i y ) C_ ( B i^i D ) /\ ( B i^i D ) = (/) ) -> ( x i^i y ) = (/) )
29	26, 27, 28	syl2anc 661	. . . . . . 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 3750	. . . . . . . 8 |- ( A u. ( C \ A ) ) = ( A u. C )
31		unen 7384	. . . . . . . 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 4321	. . . . . . 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 1219	. . . . . 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 729	. . . . . . . 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 4875	. . . . . . . . 9 |- ( C ~<_ D -> D e. _V )
36	35	ad3antlr 730	. . . . . . . 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 6376	. . . . . . . 8 |- ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
38	34, 36, 37	syl2anc 661	. . . . . . 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 3523	. . . . . . . . 9 |- ( ( x C_ B /\ y C_ D ) -> ( x u. y ) C_ ( B u. D ) )
40	39	ad2ant2l 745	. . . . . . . 8 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x u. y ) C_ ( B u. D ) )
41	40	adantl 466	. . . . . . 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 7347	. . . . . . 7 |- ( ( B u. D ) e. _V -> ( ( x u. y ) C_ ( B u. D ) -> ( x u. y ) ~<_ ( B u. D ) ) )
43	38, 41, 42	sylc 60	. . . . . 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 7359	. . . . . 6 |- ( ( ( A u. C ) ~~ ( x u. y ) /\ ( x u. y ) ~<_ ( B u. D ) ) -> ( A u. C ) ~<_ ( B u. D ) )
45	33, 43, 44	syl2anc 661	. . . . 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 434	. . . 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 1691	. . 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 218	. 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 184   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   _Vcvv 2967   \ cdif 3320   u. cun 3321   i^i cin 3322   C_ wss 3323   (/)c0 3632   class class class wbr 4287   ~~ cen 7299   ~<_ cdom 7300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-en 7303  df-dom 7304

This theorem is referenced by:  domunsncan  7403  domunsn  7453  sucdom2  7499  unxpdom2  7513  sucxpdom  7514  fodomfi  7582  uncdadom  8332  cdadom1  8347