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

Theorem reghmph 22085
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 22068 . 2 (𝐽𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2 n0 4230 . . 3 ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3 hmeocn 22052 . . . . . . . 8 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
43adantl 482 . . . . . . 7 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5 cntop2 21533 . . . . . . 7 (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
64, 5syl 17 . . . . . 6 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7 simpll 763 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝐽 ∈ Reg)
84adantr 481 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓 ∈ (𝐽 Cn 𝐾))
9 simprl 767 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑥𝐾)
10 cnima 21557 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝑓𝑥) ∈ 𝐽)
118, 9, 10syl2anc 584 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → (𝑓𝑥) ∈ 𝐽)
12 eqid 2795 . . . . . . . . . . . . 13 𝐽 = 𝐽
13 eqid 2795 . . . . . . . . . . . . 13 𝐾 = 𝐾
1412, 13hmeof1o 22056 . . . . . . . . . . . 12 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓: 𝐽1-1-onto 𝐾)
1514ad2antlr 723 . . . . . . . . . . 11 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓: 𝐽1-1-onto 𝐾)
16 f1ocnv 6495 . . . . . . . . . . 11 (𝑓: 𝐽1-1-onto 𝐾𝑓: 𝐾1-1-onto 𝐽)
17 f1ofn 6484 . . . . . . . . . . 11 (𝑓: 𝐾1-1-onto 𝐽𝑓 Fn 𝐾)
1815, 16, 173syl 18 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑓 Fn 𝐾)
19 elssuni 4774 . . . . . . . . . . 11 (𝑥𝐾𝑥 𝐾)
2019ad2antrl 724 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑥 𝐾)
21 simprr 769 . . . . . . . . . 10 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑦𝑥)
22 fnfvima 6860 . . . . . . . . . 10 ((𝑓 Fn 𝐾𝑥 𝐾𝑦𝑥) → (𝑓𝑦) ∈ (𝑓𝑥))
2318, 20, 21, 22syl3anc 1364 . . . . . . . . 9 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → (𝑓𝑦) ∈ (𝑓𝑥))
24 regsep 21626 . . . . . . . . 9 ((𝐽 ∈ Reg ∧ (𝑓𝑥) ∈ 𝐽 ∧ (𝑓𝑦) ∈ (𝑓𝑥)) → ∃𝑤𝐽 ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
257, 11, 23, 24syl3anc 1364 . . . . . . . 8 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → ∃𝑤𝐽 ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
26 simpllr 772 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
27 simprl 767 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤𝐽)
28 hmeoima 22057 . . . . . . . . . 10 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤𝐽) → (𝑓𝑤) ∈ 𝐾)
2926, 27, 28syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑤) ∈ 𝐾)
3020, 21sseldd 3890 . . . . . . . . . . . 12 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → 𝑦 𝐾)
3130adantr 481 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 𝐾)
32 simprrl 777 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑦) ∈ 𝑤)
3318adantr 481 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 Fn 𝐾)
34 elpreima 6693 . . . . . . . . . . . 12 (𝑓 Fn 𝐾 → (𝑦 ∈ (𝑓𝑤) ↔ (𝑦 𝐾 ∧ (𝑓𝑦) ∈ 𝑤)))
3533, 34syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑦 ∈ (𝑓𝑤) ↔ (𝑦 𝐾 ∧ (𝑓𝑦) ∈ 𝑤)))
3631, 32, 35mpbir2and 709 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (𝑓𝑤))
37 imacnvcnv 5938 . . . . . . . . . 10 (𝑓𝑤) = (𝑓𝑤)
3836, 37syl6eleq 2893 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (𝑓𝑤))
39 elssuni 4774 . . . . . . . . . . . 12 (𝑤𝐽𝑤 𝐽)
4039ad2antrl 724 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤 𝐽)
4112hmeocls 22060 . . . . . . . . . . 11 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 𝐽) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
4226, 40, 41syl2anc 584 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
43 simprrr 778 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥))
4415adantr 481 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓: 𝐽1-1-onto 𝐾)
45 f1ofun 6485 . . . . . . . . . . . . 13 (𝑓: 𝐽1-1-onto 𝐾 → Fun 𝑓)
4644, 45syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → Fun 𝑓)
477adantr 481 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Reg)
48 regtop 21625 . . . . . . . . . . . . . . 15 (𝐽 ∈ Reg → 𝐽 ∈ Top)
4947, 48syl 17 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Top)
5012clsss3 21351 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
5149, 40, 50syl2anc 584 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
52 f1odm 6487 . . . . . . . . . . . . . 14 (𝑓: 𝐽1-1-onto 𝐾 → dom 𝑓 = 𝐽)
5344, 52syl 17 . . . . . . . . . . . . 13 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → dom 𝑓 = 𝐽)
5451, 53sseqtr4d 3929 . . . . . . . . . . . 12 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
55 funimass3 6689 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5646, 54, 55syl2anc 584 . . . . . . . . . . 11 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5743, 56mpbird 258 . . . . . . . . . 10 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
5842, 57eqsstrd 3926 . . . . . . . . 9 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)
59 eleq2 2871 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (𝑦𝑧𝑦 ∈ (𝑓𝑤)))
60 fveq2 6538 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓𝑤)))
6160sseq1d 3919 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥))
6259, 61anbi12d 630 . . . . . . . . . 10 (𝑧 = (𝑓𝑤) → ((𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ∈ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)))
6362rspcev 3559 . . . . . . . . 9 (((𝑓𝑤) ∈ 𝐾 ∧ (𝑦 ∈ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6429, 38, 58, 63syl12anc 833 . . . . . . . 8 ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6525, 64rexlimddv 3254 . . . . . . 7 (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6665ralrimivva 3158 . . . . . 6 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥𝐾𝑦𝑥𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
67 isreg 21624 . . . . . 6 (𝐾 ∈ Reg ↔ (𝐾 ∈ Top ∧ ∀𝑥𝐾𝑦𝑥𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
686, 66, 67sylanbrc 583 . . . . 5 ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Reg)
6968expcom 414 . . . 4 (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
7069exlimiv 1908 . . 3 (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
712, 70sylbi 218 . 2 ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
721, 71sylbi 218 1 (𝐽𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wex 1761  wcel 2081  wne 2984  wral 3105  wrex 3106  wss 3859  c0 4211   cuni 4745   class class class wbr 4962  ccnv 5442  dom cdm 5443  cima 5446  Fun wfun 6219   Fn wfn 6220  1-1-ontowf1o 6224  cfv 6225  (class class class)co 7016  Topctop 21185  clsccl 21310   Cn ccn 21516  Regcreg 21601  Homeochmeo 22045  chmph 22046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-1st 7545  df-2nd 7546  df-1o 7953  df-map 8258  df-top 21186  df-topon 21203  df-cld 21311  df-cls 21313  df-cn 21519  df-reg 21608  df-hmeo 22047  df-hmph 22048
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator