Proof of Theorem cldregopn
Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | clscld 23036 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽)) |
3 | | eqcom 2733 |
. . . . 5
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
4 | 3 | biimpi 215 |
. . . 4
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
5 | | fveq2 6890 |
. . . . 5
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → ((int‘𝐽)‘𝑐) = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
6 | 5 | rspceeqv 3629 |
. . . 4
⊢
((((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
7 | 2, 4, 6 | syl2an 594 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
8 | 7 | ex 411 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |
9 | | cldrcl 23015 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
10 | 1 | cldss 23018 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝑐 ⊆ 𝑋) |
11 | 1 | ntrss2 23046 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
12 | 9, 10, 11 | syl2anc 582 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
13 | 1 | clsss2 23061 |
. . . . . . . 8
⊢ ((𝑐 ∈ (Clsd‘𝐽) ∧ ((int‘𝐽)‘𝑐) ⊆ 𝑐) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
14 | 12, 13 | mpdan 685 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
15 | 1 | ntrss 23044 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
16 | 9, 10, 14, 15 | syl3anc 1368 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
17 | 1 | ntridm 23057 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
18 | 9, 10, 17 | syl2anc 582 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
19 | 1 | ntrss3 23049 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
20 | 9, 10, 19 | syl2anc 582 |
. . . . . . . . 9
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
21 | 1 | clsss3 23048 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
22 | 9, 20, 21 | syl2anc 582 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
23 | 1 | sscls 23045 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
24 | 9, 20, 23 | syl2anc 582 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
25 | 1 | ntrss 23044 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧
((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
26 | 9, 22, 24, 25 | syl3anc 1368 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
27 | 18, 26 | eqsstrrd 4018 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
28 | 16, 27 | eqssd 3996 |
. . . . 5
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
29 | 28 | adantl 480 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
30 | | 2fveq3 6895 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
31 | | id 22 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → 𝐴 = ((int‘𝐽)‘𝑐)) |
32 | 30, 31 | eqeq12d 2742 |
. . . 4
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐))) |
33 | 29, 32 | syl5ibrcom 246 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
34 | 33 | rexlimdva 3145 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
35 | 8, 34 | impbid 211 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |