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 𝑥𝐴 𝐵 ∧ ( 𝐶𝐴𝐷𝐴 ∧ ( 𝐶𝐷 ) = ∅ ) ) → ( 𝑥𝐶 𝐵 𝑥𝐷 𝐵 ) = ∅ )