Step | Hyp | Ref
| Expression |
1 | | df-rab 2921 |
. . . . . 6
⊢ {𝑧 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑧} = {𝑧 ∣ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)} |
2 | | clscld.1 |
. . . . . . . . . . . . 13
⊢ 𝑋 = ∪
𝐽 |
3 | 2 | cldopn 20835 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑧) ∈ 𝐽) |
4 | 3 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → (𝑋 ∖ 𝑧) ∈ 𝐽) |
5 | | sscon 3744 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝑧 → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆)) |
6 | 5 | ad2antll 765 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆)) |
7 | 2 | topopn 20711 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
8 | | difexg 4808 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐽 → (𝑋 ∖ 𝑧) ∈ V) |
9 | | elpwg 4166 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∖ 𝑧) ∈ V → ((𝑋 ∖ 𝑧) ∈ 𝒫 (𝑋 ∖ 𝑆) ↔ (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top → ((𝑋 ∖ 𝑧) ∈ 𝒫 (𝑋 ∖ 𝑆) ↔ (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))) |
11 | 10 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → ((𝑋 ∖ 𝑧) ∈ 𝒫 (𝑋 ∖ 𝑆) ↔ (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆))) |
12 | 6, 11 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → (𝑋 ∖ 𝑧) ∈ 𝒫 (𝑋 ∖ 𝑆)) |
13 | 4, 12 | elind 3798 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → (𝑋 ∖ 𝑧) ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) |
14 | 2 | cldss 20833 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (Clsd‘𝐽) → 𝑧 ⊆ 𝑋) |
15 | 14 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → 𝑧 ⊆ 𝑋) |
16 | | dfss4 3858 |
. . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧) |
17 | 15, 16 | sylib 208 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧) |
18 | 17 | eqcomd 2628 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → 𝑧 = (𝑋 ∖ (𝑋 ∖ 𝑧))) |
19 | | difeq2 3722 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑋 ∖ 𝑧) → (𝑋 ∖ 𝑥) = (𝑋 ∖ (𝑋 ∖ 𝑧))) |
20 | 19 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋 ∖ 𝑧) → (𝑧 = (𝑋 ∖ 𝑥) ↔ 𝑧 = (𝑋 ∖ (𝑋 ∖ 𝑧)))) |
21 | 20 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑋 ∖ 𝑧) ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) ∧ 𝑧 = (𝑋 ∖ (𝑋 ∖ 𝑧))) → ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)) |
22 | 13, 18, 21 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)) → ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)) |
23 | 22 | ex 450 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧) → ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥))) |
24 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) |
25 | | elin 3796 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ 𝒫 (𝑋 ∖ 𝑆))) |
26 | 25 | simplbi 476 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) → 𝑥 ∈ 𝐽) |
27 | 2 | opncld 20837 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽) → (𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
28 | 24, 26, 27 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → (𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
29 | 25 | simprbi 480 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) → 𝑥 ∈ 𝒫 (𝑋 ∖ 𝑆)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → 𝑥 ∈ 𝒫 (𝑋 ∖ 𝑆)) |
31 | 30 | elpwid 4170 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → 𝑥 ⊆ (𝑋 ∖ 𝑆)) |
32 | 31 | difss2d 3740 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → 𝑥 ⊆ 𝑋) |
33 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → 𝑆 ⊆ 𝑋) |
34 | | ssconb 3743 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑋) → (𝑥 ⊆ (𝑋 ∖ 𝑆) ↔ 𝑆 ⊆ (𝑋 ∖ 𝑥))) |
35 | 32, 33, 34 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → (𝑥 ⊆ (𝑋 ∖ 𝑆) ↔ 𝑆 ⊆ (𝑋 ∖ 𝑥))) |
36 | 31, 35 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → 𝑆 ⊆ (𝑋 ∖ 𝑥)) |
37 | 28, 36 | jca 554 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → ((𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ (𝑋 ∖ 𝑥))) |
38 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑧 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽))) |
39 | | sseq2 3627 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑋 ∖ 𝑥) → (𝑆 ⊆ 𝑧 ↔ 𝑆 ⊆ (𝑋 ∖ 𝑥))) |
40 | 38, 39 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑋 ∖ 𝑥) → ((𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧) ↔ ((𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ (𝑋 ∖ 𝑥)))) |
41 | 37, 40 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) → (𝑧 = (𝑋 ∖ 𝑥) → (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧))) |
42 | 41 | rexlimdva 3031 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥) → (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧))) |
43 | 23, 42 | impbid 202 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧) ↔ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥))) |
44 | 43 | abbidv 2741 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → {𝑧 ∣ (𝑧 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑧)} = {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
45 | 1, 44 | syl5eq 2668 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → {𝑧 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑧} = {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
46 | 45 | inteqd 4480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∩ {𝑧 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑧} = ∩ {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
47 | | difexg 4808 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐽 → (𝑋 ∖ 𝑥) ∈ V) |
48 | 47 | ralrimivw 2967 |
. . . . . 6
⊢ (𝑋 ∈ 𝐽 → ∀𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) ∈ V) |
49 | | dfiin2g 4553 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) ∈ V → ∩ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) = ∩ {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
50 | 7, 48, 49 | 3syl 18 |
. . . . 5
⊢ (𝐽 ∈ Top → ∩ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) = ∩ {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
51 | 50 | adantr 481 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∩
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) = ∩ {𝑧 ∣ ∃𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑧 = (𝑋 ∖ 𝑥)}) |
52 | 46, 51 | eqtr4d 2659 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∩ {𝑧 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑧} = ∩ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥)) |
53 | 2 | clsval 20841 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑧 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑧}) |
54 | | uniiun 4573 |
. . . . . 6
⊢ ∪ (𝐽
∩ 𝒫 (𝑋 ∖
𝑆)) = ∪ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑥 |
55 | 54 | difeq2i 3725 |
. . . . 5
⊢ (𝑋 ∖ ∪ (𝐽
∩ 𝒫 (𝑋 ∖
𝑆))) = (𝑋 ∖ ∪
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑥) |
56 | 55 | a1i 11 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) = (𝑋 ∖ ∪
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑥)) |
57 | | 0opn 20709 |
. . . . . . 7
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
58 | 57 | adantr 481 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∅ ∈ 𝐽) |
59 | | 0elpw 4834 |
. . . . . . 7
⊢ ∅
∈ 𝒫 (𝑋 ∖
𝑆) |
60 | 59 | a1i 11 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∅ ∈ 𝒫 (𝑋 ∖ 𝑆)) |
61 | 58, 60 | elind 3798 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∅ ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) |
62 | | ne0i 3921 |
. . . . 5
⊢ (∅
∈ (𝐽 ∩ 𝒫
(𝑋 ∖ 𝑆)) → (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) ≠ ∅) |
63 | | iindif2 4589 |
. . . . 5
⊢ ((𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)) ≠ ∅ → ∩ 𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) = (𝑋 ∖ ∪
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑥)) |
64 | 61, 62, 63 | 3syl 18 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ∩
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥) = (𝑋 ∖ ∪
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))𝑥)) |
65 | 56, 64 | eqtr4d 2659 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) = ∩
𝑥 ∈ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))(𝑋 ∖ 𝑥)) |
66 | 52, 53, 65 | 3eqtr4d 2666 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)))) |
67 | | difssd 3738 |
. . . 4
⊢ (𝑆 ⊆ 𝑋 → (𝑋 ∖ 𝑆) ⊆ 𝑋) |
68 | 2 | ntrval 20840 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (𝑋 ∖ 𝑆) ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ 𝑆)) = ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) |
69 | 67, 68 | sylan2 491 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ 𝑆)) = ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆))) |
70 | 69 | difeq2d 3728 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆))) = (𝑋 ∖ ∪ (𝐽 ∩ 𝒫 (𝑋 ∖ 𝑆)))) |
71 | 66, 70 | eqtr4d 2659 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆)))) |