Metamath Proof Explorer

Theorem disjiun

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)

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

Proof

Step Hyp Ref Expression
1 df-disj ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2 elin ⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 ) )
3 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ↔ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 )
4 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 ↔ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 )
5 3 4 anbi12i ⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐶 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐷 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) )
6 2 5 bitri ⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ↔ ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) )
7 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ 𝐵
8 7 rmo2 ⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∃ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) )
9 an4 ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) ↔ ( ( 𝐶 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) )
10 ssralv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∈ 𝐶 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ) )
11 10 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝐶 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐶 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) )
12 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐶 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐶 ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) )
13 id ⊢ ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) )
14 13 imp ⊢ ( ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝑧 )
15 14 eleq1d ⊢ ( ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐶 ↔ 𝑧 ∈ 𝐶 ) )
16 15 biimpcd ⊢ ( 𝑥 ∈ 𝐶 → ( ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 ) )
17 16 rexlimiv ⊢ ( ∃ 𝑥 ∈ 𝐶 ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
18 12 17 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐶 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 )
19 18 ex ⊢ ( ∀ 𝑥 ∈ 𝐶 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐶 ) )
20 11 19 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐶 ) )
21 20 expimpd ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( 𝐶 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐶 ) )
22 ssralv ⊢ ( 𝐷 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∈ 𝐷 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ) )
23 22 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝐷 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐷 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) )
24 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐷 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐷 ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) )
25 14 eleq1d ⊢ ( ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 ) )
26 25 biimpcd ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐷 ) )
27 26 rexlimiv ⊢ ( ∃ 𝑥 ∈ 𝐷 ( ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐷 )
28 24 27 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐷 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐷 )
29 28 ex ⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
30 23 29 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) ∧ 𝐷 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
31 30 expimpd ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( 𝐷 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐷 ) )
32 21 31 anim12d ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( ( 𝐶 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) ) )
33 inelcm ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ )
34 32 33 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( ( 𝐶 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) )
35 34 exlimiv ⊢ ( ∃ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( ( 𝐶 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 ⊆ 𝐴 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) )
36 9 35 syl5bi ⊢ ( ∃ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) )
37 36 expd ⊢ ( ∃ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑥 = 𝑧 ) → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) → ( ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) ) )
38 8 37 sylbi ⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) → ( ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) ) )
39 38 impcom ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ( ( ∃ 𝑥 ∈ 𝐶 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐷 𝑦 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) )
40 6 39 syl5bi ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) )
41 40 necon2bd ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ( ( 𝐶 ∩ 𝐷 ) = ∅ → ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ) )
42 41 impancom ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ) )
43 42 3impa ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ) )
44 43 alimdv ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∀ 𝑦 ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ) )
45 1 44 syl5bi ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) → ( Disj 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑦 ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) ) )
46 45 impcom ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∀ 𝑦 ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) )
47 eq0 ⊢ ( ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) )
48 46 47 sylibr ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ( ∪ 𝑥 ∈ 𝐶 𝐵 ∩ ∪ 𝑥 ∈ 𝐷 𝐵 ) = ∅ )