Metamath Proof Explorer

Theorem disjxun

Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypothesis disjxun.1 ⊢ x = y → C = D
Assertion disjxun ⊢ A ∩ B = ∅ → Disj x ∈ A ∪ B C ↔ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅

Proof

Step Hyp Ref Expression
1 disjxun.1 ⊢ x = y → C = D
2 disjel ⊢ A ∩ B = ∅ ∧ x ∈ A → ¬ x ∈ B
3 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
4 3 notbid ⊢ x = y → ¬ x ∈ B ↔ ¬ y ∈ B
5 2 4 syl5ibcom ⊢ A ∩ B = ∅ ∧ x ∈ A → x = y → ¬ y ∈ B
6 5 con2d ⊢ A ∩ B = ∅ ∧ x ∈ A → y ∈ B → ¬ x = y
7 6 impr ⊢ A ∩ B = ∅ ∧ x ∈ A ∧ y ∈ B → ¬ x = y
8 biorf ⊢ ¬ x = y → C ∩ D = ∅ ↔ x = y ∨ C ∩ D = ∅
9 7 8 syl ⊢ A ∩ B = ∅ ∧ x ∈ A ∧ y ∈ B → C ∩ D = ∅ ↔ x = y ∨ C ∩ D = ∅
10 9 bicomd ⊢ A ∩ B = ∅ ∧ x ∈ A ∧ y ∈ B → x = y ∨ C ∩ D = ∅ ↔ C ∩ D = ∅
11 10 2ralbidva ⊢ A ∩ B = ∅ → ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
12 11 anbi2d ⊢ A ∩ B = ∅ → ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
13 ralunb ⊢ ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅ ↔ ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ y ∈ B x = y ∨ C ∩ D = ∅
14 13 ralbii ⊢ ∀ x ∈ A ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ y ∈ B x = y ∨ C ∩ D = ∅
15 nfv ⊢ Ⅎ z ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅
16 nfcv ⊢ Ⅎ _ x A ∪ B
17 nfv ⊢ Ⅎ x z = w
18 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ C
19 nfcsb1v ⊢ Ⅎ _ x ⦋ w / x⦌ C
20 18 19 nfin ⊢ Ⅎ _ x ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C
21 20 nfeq1 ⊢ Ⅎ x ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
22 17 21 nfor ⊢ Ⅎ x z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
23 16 22 nfralw ⊢ Ⅎ x ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
24 equequ2 ⊢ w = y → x = w ↔ x = y
25 nfcv ⊢ Ⅎ _ x y
26 nfcv ⊢ Ⅎ _ x D
27 25 26 1 csbhypf ⊢ w = y → ⦋ w / x⦌ C = D
28 27 ineq2d ⊢ w = y → C ∩ ⦋ w / x⦌ C = C ∩ D
29 28 eqeq1d ⊢ w = y → C ∩ ⦋ w / x⦌ C = ∅ ↔ C ∩ D = ∅
30 24 29 orbi12d ⊢ w = y → x = w ∨ C ∩ ⦋ w / x⦌ C = ∅ ↔ x = y ∨ C ∩ D = ∅
31 30 cbvralvw ⊢ ∀ w ∈ A ∪ B x = w ∨ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅
32 equequ1 ⊢ x = z → x = w ↔ z = w
33 csbeq1a ⊢ x = z → C = ⦋ z / x⦌ C
34 33 ineq1d ⊢ x = z → C ∩ ⦋ w / x⦌ C = ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C
35 34 eqeq1d ⊢ x = z → C ∩ ⦋ w / x⦌ C = ∅ ↔ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
36 32 35 orbi12d ⊢ x = z → x = w ∨ C ∩ ⦋ w / x⦌ C = ∅ ↔ z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
37 36 ralbidv ⊢ x = z → ∀ w ∈ A ∪ B x = w ∨ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
38 31 37 bitr3id ⊢ x = z → ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅ ↔ ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
39 15 23 38 cbvralw ⊢ ∀ x ∈ A ∀ y ∈ A ∪ B x = y ∨ C ∩ D = ∅ ↔ ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
40 r19.26 ⊢ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅
41 14 39 40 3bitr3i ⊢ ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅
42 1 disjor ⊢ Disj x ∈ A C ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅
43 42 anbi1i ⊢ Disj x ∈ A C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ A x = y ∨ C ∩ D = ∅ ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
44 12 41 43 3bitr4g ⊢ A ∩ B = ∅ → ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ Disj x ∈ A C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
45 nfv ⊢ Ⅎ w z = x ∨ ⦋ z / x⦌ C ∩ C = ∅
46 equequ2 ⊢ x = w → z = x ↔ z = w
47 csbeq1a ⊢ x = w → C = ⦋ w / x⦌ C
48 47 ineq2d ⊢ x = w → ⦋ z / x⦌ C ∩ C = ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C
49 48 eqeq1d ⊢ x = w → ⦋ z / x⦌ C ∩ C = ∅ ↔ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
50 46 49 orbi12d ⊢ x = w → z = x ∨ ⦋ z / x⦌ C ∩ C = ∅ ↔ z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
51 45 22 50 cbvralw ⊢ ∀ x ∈ A z = x ∨ ⦋ z / x⦌ C ∩ C = ∅ ↔ ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
52 equequ1 ⊢ z = y → z = x ↔ y = x
53 equcom ⊢ y = x ↔ x = y
54 52 53 bitrdi ⊢ z = y → z = x ↔ x = y
55 25 26 1 csbhypf ⊢ z = y → ⦋ z / x⦌ C = D
56 55 ineq1d ⊢ z = y → ⦋ z / x⦌ C ∩ C = D ∩ C
57 incom ⊢ D ∩ C = C ∩ D
58 56 57 eqtrdi ⊢ z = y → ⦋ z / x⦌ C ∩ C = C ∩ D
59 58 eqeq1d ⊢ z = y → ⦋ z / x⦌ C ∩ C = ∅ ↔ C ∩ D = ∅
60 54 59 orbi12d ⊢ z = y → z = x ∨ ⦋ z / x⦌ C ∩ C = ∅ ↔ x = y ∨ C ∩ D = ∅
61 60 ralbidv ⊢ z = y → ∀ x ∈ A z = x ∨ ⦋ z / x⦌ C ∩ C = ∅ ↔ ∀ x ∈ A x = y ∨ C ∩ D = ∅
62 51 61 bitr3id ⊢ z = y → ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ x ∈ A x = y ∨ C ∩ D = ∅
63 62 cbvralvw ⊢ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ y ∈ B ∀ x ∈ A x = y ∨ C ∩ D = ∅
64 ralcom ⊢ ∀ y ∈ B ∀ x ∈ A x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅
65 63 64 bitri ⊢ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅
66 65 11 bitrid ⊢ A ∩ B = ∅ → ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
67 66 anbi1d ⊢ A ∩ B = ∅ → ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ∧ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
68 ralunb ⊢ ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
69 68 ralbii ⊢ ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
70 r19.26 ⊢ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
71 69 70 bitri ⊢ ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ z ∈ B ∀ w ∈ A z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
72 disjors ⊢ Disj x ∈ B C ↔ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
73 72 anbi2ci ⊢ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ↔ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ∧ ∀ z ∈ B ∀ w ∈ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
74 67 71 73 3bitr4g ⊢ A ∩ B = ∅ → ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
75 44 74 anbi12d ⊢ A ∩ B = ∅ → ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ Disj x ∈ A C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
76 disjors ⊢ Disj x ∈ A ∪ B C ↔ ∀ z ∈ A ∪ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
77 ralunb ⊢ ∀ z ∈ A ∪ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ↔ ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
78 76 77 bitri ⊢ Disj x ∈ A ∪ B C ↔ ∀ z ∈ A ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅ ∧ ∀ z ∈ B ∀ w ∈ A ∪ B z = w ∨ ⦋ z / x⦌ C ∩ ⦋ w / x⦌ C = ∅
79 df-3an ⊢ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ↔ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
80 anandir ⊢ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ↔ Disj x ∈ A C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
81 79 80 bitri ⊢ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ↔ Disj x ∈ A C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅ ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅
82 75 78 81 3bitr4g ⊢ A ∩ B = ∅ → Disj x ∈ A ∪ B C ↔ Disj x ∈ A C ∧ Disj x ∈ B C ∧ ∀ x ∈ A ∀ y ∈ B C ∩ D = ∅