Theorem disjiun 5056

Description: A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)

Assertion

Ref	Expression
disjiun	⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅)) → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) = ∅)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem disjiun

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-disj 5035	. . . 4 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		elin 4172	. . . . . . . . . 10 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵))
3		eliun 4926	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ↔ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵)
4		eliun 4926	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 ↔ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)
5	3, 4	anbi12i 628	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵) ↔ (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵))
6	2, 5	bitri 277	. . . . . . . . 9 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) ↔ (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵))
7		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧 𝑦 ∈ 𝐵
8	7	rmo2 3873	. . . . . . . . . . 11 ⊢ (∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∃𝑧∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧))
9		an4 654	. . . . . . . . . . . . 13 ⊢ (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)) ↔ ((𝐶 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) ∧ (𝐷 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)))
10		ssralv 4036	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → ∀𝑥 ∈ 𝐶 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧)))
11	10	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝐶 ⊆ 𝐴) → ∀𝑥 ∈ 𝐶 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧))
12		r19.29 3257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑥 ∈ 𝐶 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐶 ((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵))
13		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (𝑦 ∈ 𝐵 → 𝑥 = 𝑧))
14	13	imp 409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑧)
15	14	eleq1d 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶))
16	15	biimpcd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐶 → (((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐶))
17	16	rexlimiv 3283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 ∈ 𝐶 ((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐶)
18	12, 17	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑥 ∈ 𝐶 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐶)
19	18	ex 415	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐶 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐶))
20	11, 19	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝐶 ⊆ 𝐴) → (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐶))
21	20	expimpd 456	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → ((𝐶 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐶))
22		ssralv 4036	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → ∀𝑥 ∈ 𝐷 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧)))
23	22	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝐷 ⊆ 𝐴) → ∀𝑥 ∈ 𝐷 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧))
24		r19.29 3257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑥 ∈ 𝐷 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐷 ((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵))
25	14	eleq1d 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
26	25	biimpcd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐷 → (((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐷))
27	26	rexlimiv 3283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 ∈ 𝐷 ((𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐷)
28	24, 27	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑥 ∈ 𝐷 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐷)
29	28	ex 415	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝐷 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐷))
30	23, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) ∧ 𝐷 ⊆ 𝐴) → (∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐷))
31	30	expimpd 456	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → ((𝐷 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐷))
32	21, 31	anim12d 610	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (((𝐶 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) ∧ (𝐷 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)) → (𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷)))
33		inelcm 4417	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷) → (𝐶 ∩ 𝐷) ≠ ∅)
34	32, 33	syl6 35	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (((𝐶 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) ∧ (𝐷 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)) → (𝐶 ∩ 𝐷) ≠ ∅))
35	34	exlimiv 1930	. . . . . . . . . . . . 13 ⊢ (∃𝑧∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (((𝐶 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵) ∧ (𝐷 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)) → (𝐶 ∩ 𝐷) ≠ ∅))
36	9, 35	syl5bi 244	. . . . . . . . . . . 12 ⊢ (∃𝑧∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵)) → (𝐶 ∩ 𝐷) ≠ ∅))
37	36	expd 418	. . . . . . . . . . 11 ⊢ (∃𝑧∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑥 = 𝑧) → ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → (𝐶 ∩ 𝐷) ≠ ∅)))
38	8, 37	sylbi 219	. . . . . . . . . 10 ⊢ (∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → (𝐶 ∩ 𝐷) ≠ ∅)))
39	38	impcom 410	. . . . . . . . 9 ⊢ (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ((∃𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐷 𝑦 ∈ 𝐵) → (𝐶 ∩ 𝐷) ≠ ∅))
40	6, 39	syl5bi 244	. . . . . . . 8 ⊢ (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → (𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) → (𝐶 ∩ 𝐷) ≠ ∅))
41	40	necon2bd 3035	. . . . . . 7 ⊢ (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ((𝐶 ∩ 𝐷) = ∅ → ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵)))
42	41	impancom 454	. . . . . 6 ⊢ (((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴) ∧ (𝐶 ∩ 𝐷) = ∅) → (∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵)))
43	42	3impa 1106	. . . . 5 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅) → (∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵)))
44	43	alimdv 1916	. . . 4 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅) → (∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∀𝑦 ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵)))
45	1, 44	syl5bi 244	. . 3 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅) → (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵)))
46	45	impcom 410	. 2 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅)) → ∀𝑦 ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵))
47		eq0 4311	. 2 ⊢ ((∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵))
48	46, 47	sylibr 236	1 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ (𝐶 ∩ 𝐷) = ∅)) → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083  ∀wal 1534   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∀wral 3141  ∃wrex 3142  ∃*wrmo 3144   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  ∪ ciun 4922  Disj wdisj 5034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rmo 3149  df-v 3499  df-dif 3942  df-in 3946  df-ss 3955  df-nul 4295  df-iun 4924  df-disj 5035

This theorem is referenced by:  disjxiun  5066  fsumiun  15179  uniioombllem4  24190  disjiun2  41326  sge0iunmptlemfi  42702