Theorem undom 7602

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 7519	. . . . . . 7 |- Rel ~<_
2	1	brrelex2i 5040	. . . . . 6 |- ( A ~<_ B -> B e. _V )
3		domeng 7527	. . . . . 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 5039	. . . . . . 7 |- ( C ~<_ D -> C e. _V )
7		difss 3631	. . . . . . 7 |- ( C \ A ) C_ C
8		ssdomg 7558	. . . . . . 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 7565	. . . . . 6 |- ( ( ( C \ A ) ~<_ C /\ C ~<_ D ) -> ( C \ A ) ~<_ D )
11	9, 10	mpancom 669	. . . . 5 |- ( C ~<_ D -> ( C \ A ) ~<_ D )
12	1	brrelex2i 5040	. . . . . . 7 |- ( ( C \ A ) ~<_ D -> D e. _V )
13		domeng 7527	. . . . . . 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 1957	. . 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 3899	. . . . . . . 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 3725	. . . . . . . . . 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 3817	. . . . . . . 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 3903	. . . . . . . 8 |- ( A u. ( C \ A ) ) = ( A u. C )
31		unen 7595	. . . . . . . 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 4481	. . . . . . 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 1229	. . . . . 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 5040	. . . . . . . . 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 6583	. . . . . . . 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 3676	. . . . . . . . 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 7558	. . . . . . 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 7570	. . . . . 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 1701	. . 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 1379   E.wex 1596   e. wcel 1767   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   (/)c0 3785   class class class wbr 4447   ~~ cen 7510   ~<_ cdom 7511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-en 7514  df-dom 7515

This theorem is referenced by:  domunsncan  7614  domunsn  7664  sucdom2  7711  unxpdom2  7725  sucxpdom  7726  fodomfi  7795  uncdadom  8547  cdadom1  8562