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

Theorem nrmhmph 21877
Description: Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.)
Assertion
Ref Expression
nrmhmph (𝐽𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))

Proof of Theorem nrmhmph
Dummy variables 𝑤 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hmph 21859 . 2 (𝐽𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2 n0 4095 . . 3 ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3 hmeocn 21843 . . . . . . . 8 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
43adantl 473 . . . . . . 7 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5 cntop2 21325 . . . . . . 7 (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
64, 5syl 17 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7 simpll 783 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm)
84adantr 472 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾))
9 simprl 787 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥𝐾)
10 cnima 21349 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝑓𝑥) ∈ 𝐽)
118, 9, 10syl2anc 579 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑥) ∈ 𝐽)
12 inss1 3992 . . . . . . . . . . 11 ((Clsd‘𝐾) ∩ 𝒫 𝑥) ⊆ (Clsd‘𝐾)
13 simprr 789 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))
1412, 13sseldi 3759 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾))
15 cnclima 21352 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (𝑓𝑦) ∈ (Clsd‘𝐽))
168, 14, 15syl2anc 579 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ∈ (Clsd‘𝐽))
17 inss2 3993 . . . . . . . . . . . 12 ((Clsd‘𝐾) ∩ 𝒫 𝑥) ⊆ 𝒫 𝑥
1817, 13sseldi 3759 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥)
1918elpwid 4327 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦𝑥)
20 imass2 5683 . . . . . . . . . 10 (𝑦𝑥 → (𝑓𝑦) ⊆ (𝑓𝑥))
2119, 20syl 17 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ⊆ (𝑓𝑥))
22 nrmsep3 21439 . . . . . . . . 9 ((𝐽 ∈ Nrm ∧ ((𝑓𝑥) ∈ 𝐽 ∧ (𝑓𝑦) ∈ (Clsd‘𝐽) ∧ (𝑓𝑦) ⊆ (𝑓𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
237, 11, 16, 21, 22syl13anc 1491 . . . . . . . 8 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
24 simpllr 793 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
25 simprl 787 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤𝐽)
26 hmeoima 21848 . . . . . . . . . 10 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤𝐽) → (𝑓𝑤) ∈ 𝐾)
2724, 25, 26syl2anc 579 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑤) ∈ 𝐾)
28 simprrl 799 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑦) ⊆ 𝑤)
29 eqid 2765 . . . . . . . . . . . . . 14 𝐽 = 𝐽
30 eqid 2765 . . . . . . . . . . . . . 14 𝐾 = 𝐾
3129, 30hmeof1o 21847 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓: 𝐽1-1-onto 𝐾)
3224, 31syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓: 𝐽1-1-onto 𝐾)
33 f1ofun 6322 . . . . . . . . . . . 12 (𝑓: 𝐽1-1-onto 𝐾 → Fun 𝑓)
3432, 33syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → Fun 𝑓)
3514adantr 472 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (Clsd‘𝐾))
3630cldss 21113 . . . . . . . . . . . . 13 (𝑦 ∈ (Clsd‘𝐾) → 𝑦 𝐾)
3735, 36syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 𝐾)
38 f1ofo 6327 . . . . . . . . . . . . 13 (𝑓: 𝐽1-1-onto 𝐾𝑓: 𝐽onto 𝐾)
39 forn 6301 . . . . . . . . . . . . 13 (𝑓: 𝐽onto 𝐾 → ran 𝑓 = 𝐾)
4032, 38, 393syl 18 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ran 𝑓 = 𝐾)
4137, 40sseqtr4d 3802 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ ran 𝑓)
42 funimass1 6149 . . . . . . . . . . 11 ((Fun 𝑓𝑦 ⊆ ran 𝑓) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4334, 41, 42syl2anc 579 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4428, 43mpd 15 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ (𝑓𝑤))
45 elssuni 4625 . . . . . . . . . . . 12 (𝑤𝐽𝑤 𝐽)
4645ad2antrl 719 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤 𝐽)
4729hmeocls 21851 . . . . . . . . . . 11 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 𝐽) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
4824, 46, 47syl2anc 579 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
49 simprrr 800 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥))
50 nrmtop 21420 . . . . . . . . . . . . . . 15 (𝐽 ∈ Nrm → 𝐽 ∈ Top)
5150ad3antrrr 721 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Top)
5229clsss3 21143 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
5351, 46, 52syl2anc 579 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
54 f1odm 6324 . . . . . . . . . . . . . 14 (𝑓: 𝐽1-1-onto 𝐾 → dom 𝑓 = 𝐽)
5532, 54syl 17 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → dom 𝑓 = 𝐽)
5653, 55sseqtr4d 3802 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
57 funimass3 6523 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5834, 56, 57syl2anc 579 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5949, 58mpbird 248 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
6048, 59eqsstrd 3799 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)
61 sseq2 3787 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (𝑦𝑧𝑦 ⊆ (𝑓𝑤)))
62 fveq2 6375 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓𝑤)))
6362sseq1d 3792 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥))
6461, 63anbi12d 624 . . . . . . . . . 10 (𝑧 = (𝑓𝑤) → ((𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)))
6564rspcev 3461 . . . . . . . . 9 (((𝑓𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6627, 44, 60, 65syl12anc 865 . . . . . . . 8 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6723, 66rexlimddv 3182 . . . . . . 7 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6867ralrimivva 3118 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
69 isnrm 21419 . . . . . 6 (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
706, 68, 69sylanbrc 578 . . . . 5 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm)
7170expcom 402 . . . 4 (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
7271exlimiv 2025 . . 3 (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
732, 72sylbi 208 . 2 ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
741, 73sylbi 208 1 (𝐽𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   cuni 4594   class class class wbr 4809  ccnv 5276  dom cdm 5277  ran crn 5278  cima 5280  Fun wfun 6062  ontowfo 6066  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  Topctop 20977  Clsdccld 21100  clsccl 21102   Cn ccn 21308  Nrmcnrm 21394  Homeochmeo 21836  chmph 21837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-1o 7764  df-map 8062  df-top 20978  df-topon 20995  df-cld 21103  df-cls 21105  df-cn 21311  df-nrm 21401  df-hmeo 21838  df-hmph 21839
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator