MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reghmph Structured version   Visualization version   GIF version

Theorem reghmph 23717
Description: Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
reghmph (𝐽𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg))

Proof of Theorem reghmph
Dummy variables 𝑤 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hmph 23700 . 2 (𝐽𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2 n0 4350 . . 3 ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3 hmeocn 23684 . . . . . . . 8 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
43adantl 480 . . . . . . 7 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5 cntop2 23165 . . . . . . 7 (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
64, 5syl 17 . . . . . 6 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7 simpll 765 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝐽 ∈ Reg)
84adantr 479 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓 ∈ (𝐽 Cn 𝐾))
9 simprl 769 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑥𝐾)
10 cnima 23189 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝑓𝑥) ∈ 𝐽)
118, 9, 10syl2anc 582 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → (𝑓𝑥) ∈ 𝐽)
12 eqid 2728 . . . . . . . . . . . . 13 𝐽 = 𝐽
13 eqid 2728 . . . . . . . . . . . . 13 𝐾 = 𝐾
1412, 13hmeof1o 23688 . . . . . . . . . . . 12 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓: 𝐽1-1-onto 𝐾)
1514ad2antlr 725 . . . . . . . . . . 11 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓: 𝐽1-1-onto 𝐾)
16 f1ocnv 6856 . . . . . . . . . . 11 (𝑓: 𝐽1-1-onto 𝐾𝑓: 𝐾1-1-onto 𝐽)
17 f1ofn 6845 . . . . . . . . . . 11 (𝑓: 𝐾1-1-onto 𝐽𝑓 Fn 𝐾)
1815, 16, 173syl 18 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓 Fn 𝐾)
19 elssuni 4944 . . . . . . . . . . 11 (𝑥𝐾𝑥 𝐾)
2019ad2antrl 726 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑥 𝐾)
21 simprr 771 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑦𝑥)
22 fnfvima 7251 . . . . . . . . . 10 ((𝑓 Fn 𝐾𝑥 𝐾𝑦𝑥) → (𝑓𝑦) ∈ (𝑓𝑥))
2318, 20, 21, 22syl3anc 1368 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → (𝑓𝑦) ∈ (𝑓𝑥))
24 regsep 23258 . . . . . . . . 9 ((𝐽 ∈ Reg ∧ (𝑓𝑥) ∈ 𝐽 ∧ (𝑓𝑦) ∈ (𝑓𝑥)) → ∃𝑤𝐽 ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
257, 11, 23, 24syl3anc 1368 . . . . . . . 8 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → ∃𝑤𝐽 ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
26 simpllr 774 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
27 simprl 769 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤𝐽)
28 hmeoima 23689 . . . . . . . . . 10 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤𝐽) → (𝑓𝑤) ∈ 𝐾)
2926, 27, 28syl2anc 582 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑤) ∈ 𝐾)
3020, 21sseldd 3983 . . . . . . . . . . . 12 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑦 𝐾)
3130adantr 479 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 𝐾)
32 simprrl 779 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑦) ∈ 𝑤)
3318adantr 479 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 Fn 𝐾)
34 elpreima 7072 . . . . . . . . . . . 12 (𝑓 Fn 𝐾 → (𝑦 ∈ (𝑓𝑤) ↔ (𝑦 𝐾 ∧ (𝑓𝑦) ∈ 𝑤)))
3533, 34syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑦 ∈ (𝑓𝑤) ↔ (𝑦 𝐾 ∧ (𝑓𝑦) ∈ 𝑤)))
3631, 32, 35mpbir2and 711 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (𝑓𝑤))
37 imacnvcnv 6215 . . . . . . . . . 10 (𝑓𝑤) = (𝑓𝑤)
3836, 37eleqtrdi 2839 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (𝑓𝑤))
39 elssuni 4944 . . . . . . . . . . . 12 (𝑤𝐽𝑤 𝐽)
4039ad2antrl 726 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤 𝐽)
4112hmeocls 23692 . . . . . . . . . . 11 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 𝐽) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
4226, 40, 41syl2anc 582 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
43 simprrr 780 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥))
4415adantr 479 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓: 𝐽1-1-onto 𝐾)
45 f1ofun 6846 . . . . . . . . . . . . 13 (𝑓: 𝐽1-1-onto 𝐾 → Fun 𝑓)
4644, 45syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → Fun 𝑓)
477adantr 479 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Reg)
48 regtop 23257 . . . . . . . . . . . . . . 15 (𝐽 ∈ Reg → 𝐽 ∈ Top)
4947, 48syl 17 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Top)
5012clsss3 22983 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
5149, 40, 50syl2anc 582 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
52 f1odm 6848 . . . . . . . . . . . . . 14 (𝑓: 𝐽1-1-onto 𝐾 → dom 𝑓 = 𝐽)
5344, 52syl 17 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → dom 𝑓 = 𝐽)
5451, 53sseqtrrd 4023 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
55 funimass3 7068 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5646, 54, 55syl2anc 582 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5743, 56mpbird 256 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
5842, 57eqsstrd 4020 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)
59 eleq2 2818 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (𝑦𝑧𝑦 ∈ (𝑓𝑤)))
60 fveq2 6902 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓𝑤)))
6160sseq1d 4013 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥))
6259, 61anbi12d 630 . . . . . . . . . 10 (𝑧 = (𝑓𝑤) → ((𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ∈ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)))
6362rspcev 3611 . . . . . . . . 9 (((𝑓𝑤) ∈ 𝐾 ∧ (𝑦 ∈ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6429, 38, 58, 63syl12anc 835 . . . . . . . 8 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6525, 64rexlimddv 3158 . . . . . . 7 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6665ralrimivva 3198 . . . . . 6 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥𝐾𝑦𝑥𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
67 isreg 23256 . . . . . 6 (𝐾 ∈ Reg ↔ (𝐾 ∈ Top ∧ ∀𝑥𝐾𝑦𝑥𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
686, 66, 67sylanbrc 581 . . . . 5 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Reg)
6968expcom 412 . . . 4 (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
7069exlimiv 1925 . . 3 (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
712, 70sylbi 216 . 2 ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
721, 71sylbi 216 1 (𝐽𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wex 1773  wcel 2098  wne 2937  wral 3058  wrex 3067  wss 3949  c0 4326   cuni 4912   class class class wbr 5152  ccnv 5681  dom cdm 5682  cima 5685  Fun wfun 6547   Fn wfn 6548  1-1-ontowf1o 6552  cfv 6553  (class class class)co 7426  Topctop 22815  clsccl 22942   Cn ccn 23148  Regcreg 23233  Homeochmeo 23677  chmph 23678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 7999  df-2nd 8000  df-1o 8493  df-map 8853  df-top 22816  df-topon 22833  df-cld 22943  df-cls 22945  df-cn 23151  df-reg 23240  df-hmeo 23679  df-hmph 23680
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator