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

Theorem nrmhmph 21645
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 21627 . 2 (𝐽𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2 n0 3964 . . 3 ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3 hmeocn 21611 . . . . . . . 8 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
43adantl 481 . . . . . . 7 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5 cntop2 21093 . . . . . . 7 (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
64, 5syl 17 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7 simpll 805 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm)
84adantr 480 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾))
9 simprl 809 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥𝐾)
10 cnima 21117 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝑓𝑥) ∈ 𝐽)
118, 9, 10syl2anc 694 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑥) ∈ 𝐽)
12 inss1 3866 . . . . . . . . . . 11 ((Clsd‘𝐾) ∩ 𝒫 𝑥) ⊆ (Clsd‘𝐾)
13 simprr 811 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))
1412, 13sseldi 3634 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾))
15 cnclima 21120 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (𝑓𝑦) ∈ (Clsd‘𝐽))
168, 14, 15syl2anc 694 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ∈ (Clsd‘𝐽))
17 inss2 3867 . . . . . . . . . . . 12 ((Clsd‘𝐾) ∩ 𝒫 𝑥) ⊆ 𝒫 𝑥
1817, 13sseldi 3634 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥)
1918elpwid 4203 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦𝑥)
20 imass2 5536 . . . . . . . . . 10 (𝑦𝑥 → (𝑓𝑦) ⊆ (𝑓𝑥))
2119, 20syl 17 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ⊆ (𝑓𝑥))
22 nrmsep3 21207 . . . . . . . . 9 ((𝐽 ∈ Nrm ∧ ((𝑓𝑥) ∈ 𝐽 ∧ (𝑓𝑦) ∈ (Clsd‘𝐽) ∧ (𝑓𝑦) ⊆ (𝑓𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
237, 11, 16, 21, 22syl13anc 1368 . . . . . . . 8 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
24 simpllr 815 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
25 simprl 809 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤𝐽)
26 hmeoima 21616 . . . . . . . . . 10 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤𝐽) → (𝑓𝑤) ∈ 𝐾)
2724, 25, 26syl2anc 694 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑤) ∈ 𝐾)
28 simprrl 821 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑦) ⊆ 𝑤)
29 eqid 2651 . . . . . . . . . . . . . 14 𝐽 = 𝐽
30 eqid 2651 . . . . . . . . . . . . . 14 𝐾 = 𝐾
3129, 30hmeof1o 21615 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓: 𝐽1-1-onto 𝐾)
3224, 31syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓: 𝐽1-1-onto 𝐾)
33 f1ofun 6177 . . . . . . . . . . . 12 (𝑓: 𝐽1-1-onto 𝐾 → Fun 𝑓)
3432, 33syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → Fun 𝑓)
3514adantr 480 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (Clsd‘𝐾))
3630cldss 20881 . . . . . . . . . . . . 13 (𝑦 ∈ (Clsd‘𝐾) → 𝑦 𝐾)
3735, 36syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 𝐾)
38 f1ofo 6182 . . . . . . . . . . . . 13 (𝑓: 𝐽1-1-onto 𝐾𝑓: 𝐽onto 𝐾)
39 forn 6156 . . . . . . . . . . . . 13 (𝑓: 𝐽onto 𝐾 → ran 𝑓 = 𝐾)
4032, 38, 393syl 18 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ran 𝑓 = 𝐾)
4137, 40sseqtr4d 3675 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ ran 𝑓)
42 funimass1 6009 . . . . . . . . . . 11 ((Fun 𝑓𝑦 ⊆ ran 𝑓) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4334, 41, 42syl2anc 694 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4428, 43mpd 15 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ (𝑓𝑤))
45 elssuni 4499 . . . . . . . . . . . 12 (𝑤𝐽𝑤 𝐽)
4645ad2antrl 764 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤 𝐽)
4729hmeocls 21619 . . . . . . . . . . 11 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 𝐽) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
4824, 46, 47syl2anc 694 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
49 simprrr 822 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥))
50 nrmtop 21188 . . . . . . . . . . . . . . 15 (𝐽 ∈ Nrm → 𝐽 ∈ Top)
5150ad3antrrr 766 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Top)
5229clsss3 20911 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
5351, 46, 52syl2anc 694 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
54 f1odm 6179 . . . . . . . . . . . . . 14 (𝑓: 𝐽1-1-onto 𝐾 → dom 𝑓 = 𝐽)
5532, 54syl 17 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → dom 𝑓 = 𝐽)
5653, 55sseqtr4d 3675 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
57 funimass3 6373 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5834, 56, 57syl2anc 694 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5949, 58mpbird 247 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
6048, 59eqsstrd 3672 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)
61 sseq2 3660 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (𝑦𝑧𝑦 ⊆ (𝑓𝑤)))
62 fveq2 6229 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓𝑤)))
6362sseq1d 3665 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥))
6461, 63anbi12d 747 . . . . . . . . . 10 (𝑧 = (𝑓𝑤) → ((𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)))
6564rspcev 3340 . . . . . . . . 9 (((𝑓𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6627, 44, 60, 65syl12anc 1364 . . . . . . . 8 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6723, 66rexlimddv 3064 . . . . . . 7 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6867ralrimivva 3000 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
69 isnrm 21187 . . . . . 6 (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
706, 68, 69sylanbrc 699 . . . . 5 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm)
7170expcom 450 . . . 4 (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
7271exlimiv 1898 . . 3 (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
732, 72sylbi 207 . 2 ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
741, 73sylbi 207 1 (𝐽𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191   cuni 4468   class class class wbr 4685  ccnv 5142  dom cdm 5143  ran crn 5144  cima 5146  Fun wfun 5920  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Topctop 20746  Clsdccld 20868  clsccl 20870   Cn ccn 21076  Nrmcnrm 21162  Homeochmeo 21604  chmph 21605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-1o 7605  df-map 7901  df-top 20747  df-topon 20764  df-cld 20871  df-cls 20873  df-cn 21079  df-nrm 21169  df-hmeo 21606  df-hmph 21607
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator