Theorem undom 7598

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 7515	. . . . . . 7 |- Rel ~<_
2	1	brrelex2i 5030	. . . . . 6 |- ( A ~<_ B -> B e. _V )
3		domeng 7523	. . . . . 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 5029	. . . . . . 7 |- ( C ~<_ D -> C e. _V )
7		difss 3617	. . . . . . 7 |- ( C \ A ) C_ C
8		ssdomg 7554	. . . . . . 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 7561	. . . . . 6 |- ( ( ( C \ A ) ~<_ C /\ C ~<_ D ) -> ( C \ A ) ~<_ D )
11	9, 10	mpancom 667	. . . . 5 |- ( C ~<_ D -> ( C \ A ) ~<_ D )
12	1	brrelex2i 5030	. . . . . . 7 |- ( ( C \ A ) ~<_ D -> D e. _V )
13		domeng 7523	. . . . . . 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 564	. . 3 |- ( ( A ~<_ B /\ C ~<_ D ) -> ( E. x ( A ~~ x /\ x C_ B ) /\ E. y ( ( C \ A ) ~~ y /\ y C_ D ) ) )
18	17	adantr 463	. 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 1993	. . 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 3888	. . . . . . . 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 3711	. . . . . . . . . 10 |- ( ( x C_ B /\ y C_ D ) -> ( x i^i y ) C_ ( B i^i D ) )
25	24	ad2ant2l 743	. . . . . . . . 9 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x i^i y ) C_ ( B i^i D ) )
26	25	adantl 464	. . . . . . . 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 753	. . . . . . . 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 3816	. . . . . . . 8 |- ( ( ( x i^i y ) C_ ( B i^i D ) /\ ( B i^i D ) = (/) ) -> ( x i^i y ) = (/) )
29	26, 27, 28	syl2anc 659	. . . . . . 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 3892	. . . . . . . 8 |- ( A u. ( C \ A ) ) = ( A u. C )
31		unen 7591	. . . . . . . 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 4473	. . . . . . 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 1227	. . . . . 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 727	. . . . . . . 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 5030	. . . . . . . . 9 |- ( C ~<_ D -> D e. _V )
36	35	ad3antlr 728	. . . . . . . 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 6574	. . . . . . . 8 |- ( ( B e. _V /\ D e. _V ) -> ( B u. D ) e. _V )
38	34, 36, 37	syl2anc 659	. . . . . . 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 3662	. . . . . . . . 9 |- ( ( x C_ B /\ y C_ D ) -> ( x u. y ) C_ ( B u. D ) )
40	39	ad2ant2l 743	. . . . . . . 8 |- ( ( ( A ~~ x /\ x C_ B ) /\ ( ( C \ A ) ~~ y /\ y C_ D ) ) -> ( x u. y ) C_ ( B u. D ) )
41	40	adantl 464	. . . . . . 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 7554	. . . . . . 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 7566	. . . . . 6 |- ( ( ( A u. C ) ~~ ( x u. y ) /\ ( x u. y ) ~<_ ( B u. D ) ) -> ( A u. C ) ~<_ ( B u. D ) )
45	33, 43, 44	syl2anc 659	. . . . 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 432	. . . 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 1730	. . 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 367   = wceq 1398   E.wex 1617   e. wcel 1823   _Vcvv 3106   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3783   class class class wbr 4439   ~~ cen 7506   ~<_ cdom 7507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-en 7510  df-dom 7511

This theorem is referenced by:  domunsncan  7610  domunsn  7660  sucdom2  7707  unxpdom2  7721  sucxpdom  7722  fodomfi  7791  uncdadom  8542  cdadom1  8557