Proof of Theorem cldregopn
Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | clscld 20851 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽)) |
3 | | eqcom 2629 |
. . . . 5
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
4 | 3 | biimpi 206 |
. . . 4
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
5 | | fveq2 6191 |
. . . . . 6
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → ((int‘𝐽)‘𝑐) = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
6 | 5 | eqeq2d 2632 |
. . . . 5
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → (𝐴 = ((int‘𝐽)‘𝑐) ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴)))) |
7 | 6 | rspcev 3309 |
. . . 4
⊢
((((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
8 | 2, 4, 7 | syl2an 494 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
9 | 8 | ex 450 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |
10 | | cldrcl 20830 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
11 | 1 | cldss 20833 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝑐 ⊆ 𝑋) |
12 | 1 | ntrss2 20861 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
13 | 10, 11, 12 | syl2anc 693 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
14 | 1 | clsss2 20876 |
. . . . . . . 8
⊢ ((𝑐 ∈ (Clsd‘𝐽) ∧ ((int‘𝐽)‘𝑐) ⊆ 𝑐) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
15 | 13, 14 | mpdan 702 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
16 | 1 | ntrss 20859 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
17 | 10, 11, 15, 16 | syl3anc 1326 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
18 | 1 | ntridm 20872 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
19 | 10, 11, 18 | syl2anc 693 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
20 | 1 | ntrss3 20864 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
21 | 10, 11, 20 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
22 | 1 | clsss3 20863 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
23 | 10, 21, 22 | syl2anc 693 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
24 | 1 | sscls 20860 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
25 | 10, 21, 24 | syl2anc 693 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
26 | 1 | ntrss 20859 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧
((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
27 | 10, 23, 25, 26 | syl3anc 1326 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
28 | 19, 27 | eqsstr3d 3640 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
29 | 17, 28 | eqssd 3620 |
. . . . 5
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
30 | 29 | adantl 482 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
31 | | fveq2 6191 |
. . . . . 6
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((cls‘𝐽)‘𝐴) = ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
32 | 31 | fveq2d 6195 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
33 | | id 22 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → 𝐴 = ((int‘𝐽)‘𝑐)) |
34 | 32, 33 | eqeq12d 2637 |
. . . 4
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐))) |
35 | 30, 34 | syl5ibrcom 237 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
36 | 35 | rexlimdva 3031 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
37 | 9, 36 | impbid 202 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |