Proof of Theorem cldregopn
Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | clscld 22208 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽)) |
3 | | eqcom 2745 |
. . . . 5
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
4 | 3 | biimpi 215 |
. . . 4
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
5 | | fveq2 6766 |
. . . . 5
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → ((int‘𝐽)‘𝑐) = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
6 | 5 | rspceeqv 3574 |
. . . 4
⊢
((((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
7 | 2, 4, 6 | syl2an 596 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
8 | 7 | ex 413 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |
9 | | cldrcl 22187 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
10 | 1 | cldss 22190 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝑐 ⊆ 𝑋) |
11 | 1 | ntrss2 22218 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
13 | 1 | clsss2 22233 |
. . . . . . . 8
⊢ ((𝑐 ∈ (Clsd‘𝐽) ∧ ((int‘𝐽)‘𝑐) ⊆ 𝑐) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
14 | 12, 13 | mpdan 684 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
15 | 1 | ntrss 22216 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
16 | 9, 10, 14, 15 | syl3anc 1370 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
17 | 1 | ntridm 22229 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
18 | 9, 10, 17 | syl2anc 584 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
19 | 1 | ntrss3 22221 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
20 | 9, 10, 19 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
21 | 1 | clsss3 22220 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
22 | 9, 20, 21 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
23 | 1 | sscls 22217 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
24 | 9, 20, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
25 | 1 | ntrss 22216 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧
((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
26 | 9, 22, 24, 25 | syl3anc 1370 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
27 | 18, 26 | eqsstrrd 3959 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
28 | 16, 27 | eqssd 3937 |
. . . . 5
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
29 | 28 | adantl 482 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
30 | | 2fveq3 6771 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
31 | | id 22 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → 𝐴 = ((int‘𝐽)‘𝑐)) |
32 | 30, 31 | eqeq12d 2754 |
. . . 4
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐))) |
33 | 29, 32 | syl5ibrcom 246 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
34 | 33 | rexlimdva 3211 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
35 | 8, 34 | impbid 211 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |