Metamath Proof Explorer

Theorem disjxun

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

Ref Expression
Hypothesis disjxun.1 ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 )
Assertion disjxun ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( Disj 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 ↔ ( Disj 𝑥 ∈ 𝐴 𝐶 ∧ Disj 𝑥 ∈ 𝐵 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ∅ ) ) )

Proof

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