Proof of Theorem conndisj
Step | Hyp | Ref
| Expression |
1 | | conclo.3 |
. 2
⊢ (𝜑 → 𝐴 ≠ ∅) |
2 | | conclo.2 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝐽) |
3 | | elssuni 4403 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) |
5 | | iscon.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
6 | 4, 5 | syl6sseqr 3615 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
7 | | conndisj.6 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
8 | | uneqdifeq 4009 |
. . . . 5
⊢ ((𝐴 ⊆ 𝑋 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝑋 ↔ (𝑋 ∖ 𝐴) = 𝐵)) |
9 | 6, 7, 8 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝐴 ∪ 𝐵) = 𝑋 ↔ (𝑋 ∖ 𝐴) = 𝐵)) |
10 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ 𝐴) = 𝐵) |
11 | 10 | difeq2d 3690 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ (𝑋 ∖ 𝐴)) = (𝑋 ∖ 𝐵)) |
12 | | dfss4 3820 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴) |
13 | 6, 12 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴) |
15 | | conclo.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ Con) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐽 ∈ Con) |
17 | | conndisj.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝐽) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐵 ∈ 𝐽) |
19 | | conndisj.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ ∅) |
20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐵 ≠ ∅) |
21 | 5 | iscon 21026 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Con ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋})) |
22 | 21 | simplbi 475 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Con → 𝐽 ∈ Top) |
23 | 15, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ Top) |
24 | 5 | opncld 20647 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝑋 ∖ 𝐴) ∈ (Clsd‘𝐽)) |
25 | 23, 2, 24 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∖ 𝐴) ∈ (Clsd‘𝐽)) |
26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ 𝐴) ∈ (Clsd‘𝐽)) |
27 | 10, 26 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐵 ∈ (Clsd‘𝐽)) |
28 | 5, 16, 18, 20, 27 | conclo 21028 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐵 = 𝑋) |
29 | 28 | difeq2d 3690 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ 𝐵) = (𝑋 ∖ 𝑋)) |
30 | | difid 3902 |
. . . . . . 7
⊢ (𝑋 ∖ 𝑋) = ∅ |
31 | 29, 30 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → (𝑋 ∖ 𝐵) = ∅) |
32 | 11, 14, 31 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∖ 𝐴) = 𝐵) → 𝐴 = ∅) |
33 | 32 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑋 ∖ 𝐴) = 𝐵 → 𝐴 = ∅)) |
34 | 9, 33 | sylbid 229 |
. . 3
⊢ (𝜑 → ((𝐴 ∪ 𝐵) = 𝑋 → 𝐴 = ∅)) |
35 | 34 | necon3d 2803 |
. 2
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐴 ∪ 𝐵) ≠ 𝑋)) |
36 | 1, 35 | mpd 15 |
1
⊢ (𝜑 → (𝐴 ∪ 𝐵) ≠ 𝑋) |