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=∅→Disjx∈A∪BC↔Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩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∈Bx=y∨C∩D=∅↔∀x∈A∀y∈BC∩D=∅
12 11 anbi2d ⊢A∩B=∅→∀x∈A∀y∈Ax=y∨C∩D=∅∧∀x∈A∀y∈Bx=y∨C∩D=∅↔∀x∈A∀y∈Ax=y∨C∩D=∅∧∀x∈A∀y∈BC∩D=∅
13 ralunb ⊢∀y∈A∪Bx=y∨C∩D=∅↔∀y∈Ax=y∨C∩D=∅∧∀y∈Bx=y∨C∩D=∅
14 13 ralbii ⊢∀x∈A∀y∈A∪Bx=y∨C∩D=∅↔∀x∈A∀y∈Ax=y∨C∩D=∅∧∀y∈Bx=y∨C∩D=∅
15 nfv ⊢Ⅎz∀y∈A∪Bx=y∨C∩D=∅
16 nfcv ⊢Ⅎ_xA∪B
17 nfv ⊢Ⅎxz=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 ⊢Ⅎxz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
23 16 22 nfralw ⊢Ⅎx∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
24 equequ2 ⊢w=y→x=w↔x=y
25 nfcv ⊢Ⅎ_xy
26 nfcv ⊢Ⅎ_xD
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∪Bx=w∨C∩⦋w/x⦌C=∅↔∀y∈A∪Bx=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∪Bx=w∨C∩⦋w/x⦌C=∅↔∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
38 31 37 bitr3id ⊢x=z→∀y∈A∪Bx=y∨C∩D=∅↔∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
39 15 23 38 cbvralw ⊢∀x∈A∀y∈A∪Bx=y∨C∩D=∅↔∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
40 r19.26 ⊢∀x∈A∀y∈Ax=y∨C∩D=∅∧∀y∈Bx=y∨C∩D=∅↔∀x∈A∀y∈Ax=y∨C∩D=∅∧∀x∈A∀y∈Bx=y∨C∩D=∅
41 14 39 40 3bitr3i ⊢∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀x∈A∀y∈Ax=y∨C∩D=∅∧∀x∈A∀y∈Bx=y∨C∩D=∅
42 1 disjor ⊢Disjx∈AC↔∀x∈A∀y∈Ax=y∨C∩D=∅
43 42 anbi1i ⊢Disjx∈AC∧∀x∈A∀y∈BC∩D=∅↔∀x∈A∀y∈Ax=y∨C∩D=∅∧∀x∈A∀y∈BC∩D=∅
44 12 41 43 3bitr4g ⊢A∩B=∅→∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔Disjx∈AC∧∀x∈A∀y∈BC∩D=∅
45 nfv ⊢Ⅎwz=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∈Az=x∨⦋z/x⦌C∩C=∅↔∀w∈Az=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∈Az=x∨⦋z/x⦌C∩C=∅↔∀x∈Ax=y∨C∩D=∅
62 51 61 bitr3id ⊢z=y→∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀x∈Ax=y∨C∩D=∅
63 62 cbvralvw ⊢∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀y∈B∀x∈Ax=y∨C∩D=∅
64 ralcom ⊢∀y∈B∀x∈Ax=y∨C∩D=∅↔∀x∈A∀y∈Bx=y∨C∩D=∅
65 63 64 bitri ⊢∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀x∈A∀y∈Bx=y∨C∩D=∅
66 65 11 bitrid ⊢A∩B=∅→∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀x∈A∀y∈BC∩D=∅
67 66 anbi1d ⊢A∩B=∅→∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀x∈A∀y∈BC∩D=∅∧∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
68 ralunb ⊢∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
69 68 ralbii ⊢∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
70 r19.26 ⊢∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
71 69 70 bitri ⊢∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀z∈B∀w∈Az=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
72 disjors ⊢Disjx∈BC↔∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
73 72 anbi2ci ⊢Disjx∈BC∧∀x∈A∀y∈BC∩D=∅↔∀x∈A∀y∈BC∩D=∅∧∀z∈B∀w∈Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
74 67 71 73 3bitr4g ⊢A∩B=∅→∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔Disjx∈BC∧∀x∈A∀y∈BC∩D=∅
75 44 74 anbi12d ⊢A∩B=∅→∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔Disjx∈AC∧∀x∈A∀y∈BC∩D=∅∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅
76 disjors ⊢Disjx∈A∪BC↔∀z∈A∪B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
77 ralunb ⊢∀z∈A∪B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅↔∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
78 76 77 bitri ⊢Disjx∈A∪BC↔∀z∈A∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅∧∀z∈B∀w∈A∪Bz=w∨⦋z/x⦌C∩⦋w/x⦌C=∅
79 df-3an ⊢Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅↔Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅
80 anandir ⊢Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅↔Disjx∈AC∧∀x∈A∀y∈BC∩D=∅∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅
81 79 80 bitri ⊢Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅↔Disjx∈AC∧∀x∈A∀y∈BC∩D=∅∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅
82 75 78 81 3bitr4g ⊢A∩B=∅→Disjx∈A∪BC↔Disjx∈AC∧Disjx∈BC∧∀x∈A∀y∈BC∩D=∅