Proof of Theorem cldregopn
Step | Hyp | Ref
| Expression |
1 | | opnregcld.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | clscld 20661 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽)) |
3 | | eqcom 2617 |
. . . . 5
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
4 | 3 | biimpi 205 |
. . . 4
⊢
(((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → ((int‘𝐽)‘𝑐) = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) |
6 | 5 | eqeq2d 2620 |
. . . . 5
⊢ (𝑐 = ((cls‘𝐽)‘𝐴) → (𝐴 = ((int‘𝐽)‘𝑐) ↔ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴)))) |
7 | 6 | rspcev 3282 |
. . . 4
⊢
((((cls‘𝐽)‘𝐴) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((int‘𝐽)‘((cls‘𝐽)‘𝐴))) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
8 | 2, 4, 7 | syl2an 493 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴) → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)) |
9 | 8 | ex 449 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 → ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |
10 | | cldrcl 20640 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
11 | 1 | cldss 20643 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → 𝑐 ⊆ 𝑋) |
12 | 1 | ntrss2 20671 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑐) |
14 | 1 | clsss2 20686 |
. . . . . . . 8
⊢ ((𝑐 ∈ (Clsd‘𝐽) ∧ ((int‘𝐽)‘𝑐) ⊆ 𝑐) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
15 | 13, 14 | mpdan 699 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) |
16 | 1 | ntrss 20669 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋 ∧ ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
17 | 10, 11, 15, 16 | syl3anc 1318 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) ⊆ ((int‘𝐽)‘𝑐)) |
18 | 1 | ntridm 20682 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
19 | 10, 11, 18 | syl2anc 691 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) = ((int‘𝐽)‘𝑐)) |
20 | 1 | ntrss3 20674 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑐 ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
21 | 10, 11, 20 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ 𝑋) |
22 | 1 | clsss3 20673 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
23 | 10, 21, 22 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋) |
24 | 1 | sscls 20670 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧
((int‘𝐽)‘𝑐) ⊆ 𝑋) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
25 | 10, 21, 24 | syl2anc 691 |
. . . . . . . 8
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
26 | 1 | ntrss 20669 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧
((cls‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑐) ⊆ ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
27 | 10, 23, 25, 26 | syl3anc 1318 |
. . . . . . 7
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((int‘𝐽)‘𝑐)) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
28 | 19, 27 | eqsstr3d 3603 |
. . . . . 6
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘𝑐) ⊆ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
29 | 17, 28 | eqssd 3585 |
. . . . 5
⊢ (𝑐 ∈ (Clsd‘𝐽) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
30 | 29 | adantl 481 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐)) |
31 | | fveq2 6103 |
. . . . . 6
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((cls‘𝐽)‘𝐴) = ((cls‘𝐽)‘((int‘𝐽)‘𝑐))) |
32 | 31 | fveq2d 6107 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐)))) |
33 | | id 22 |
. . . . 5
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → 𝐴 = ((int‘𝐽)‘𝑐)) |
34 | 32, 33 | eqeq12d 2625 |
. . . 4
⊢ (𝐴 = ((int‘𝐽)‘𝑐) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ((int‘𝐽)‘((cls‘𝐽)‘((int‘𝐽)‘𝑐))) = ((int‘𝐽)‘𝑐))) |
35 | 30, 34 | syl5ibrcom 236 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑐 ∈ (Clsd‘𝐽)) → (𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
36 | 35 | rexlimdva 3013 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐) → ((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴)) |
37 | 9, 36 | impbid 201 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐))) |