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

Theorem nrmhmph 23648
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 23630 . 2 (𝐽𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅)
2 n0 4341 . . 3 ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾))
3 hmeocn 23614 . . . . . . . 8 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾))
43adantl 481 . . . . . . 7 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾))
5 cntop2 23095 . . . . . . 7 (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
64, 5syl 17 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top)
7 simpll 764 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm)
84adantr 480 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾))
9 simprl 768 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥𝐾)
10 cnima 23119 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥𝐾) → (𝑓𝑥) ∈ 𝐽)
118, 9, 10syl2anc 583 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑥) ∈ 𝐽)
12 simprr 770 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))
1312elin1d 4193 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾))
14 cnclima 23122 . . . . . . . . . 10 ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (𝑓𝑦) ∈ (Clsd‘𝐽))
158, 13, 14syl2anc 583 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ∈ (Clsd‘𝐽))
1612elin2d 4194 . . . . . . . . . . 11 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥)
1716elpwid 4606 . . . . . . . . . 10 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦𝑥)
18 imass2 6094 . . . . . . . . . 10 (𝑦𝑥 → (𝑓𝑦) ⊆ (𝑓𝑥))
1917, 18syl 17 . . . . . . . . 9 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (𝑓𝑦) ⊆ (𝑓𝑥))
20 nrmsep3 23209 . . . . . . . . 9 ((𝐽 ∈ Nrm ∧ ((𝑓𝑥) ∈ 𝐽 ∧ (𝑓𝑦) ∈ (Clsd‘𝐽) ∧ (𝑓𝑦) ⊆ (𝑓𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
217, 11, 15, 19, 20syl13anc 1369 . . . . . . . 8 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤𝐽 ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
22 simpllr 773 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾))
23 simprl 768 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤𝐽)
24 hmeoima 23619 . . . . . . . . . 10 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤𝐽) → (𝑓𝑤) ∈ 𝐾)
2522, 23, 24syl2anc 583 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑤) ∈ 𝐾)
26 simprrl 778 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓𝑦) ⊆ 𝑤)
27 eqid 2726 . . . . . . . . . . . . . 14 𝐽 = 𝐽
28 eqid 2726 . . . . . . . . . . . . . 14 𝐾 = 𝐾
2927, 28hmeof1o 23618 . . . . . . . . . . . . 13 (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓: 𝐽1-1-onto 𝐾)
3022, 29syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑓: 𝐽1-1-onto 𝐾)
31 f1ofun 6828 . . . . . . . . . . . 12 (𝑓: 𝐽1-1-onto 𝐾 → Fun 𝑓)
3230, 31syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → Fun 𝑓)
3313adantr 480 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ∈ (Clsd‘𝐾))
3428cldss 22883 . . . . . . . . . . . . 13 (𝑦 ∈ (Clsd‘𝐾) → 𝑦 𝐾)
3533, 34syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 𝐾)
36 f1ofo 6833 . . . . . . . . . . . . 13 (𝑓: 𝐽1-1-onto 𝐾𝑓: 𝐽onto 𝐾)
37 forn 6801 . . . . . . . . . . . . 13 (𝑓: 𝐽onto 𝐾 → ran 𝑓 = 𝐾)
3830, 36, 373syl 18 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ran 𝑓 = 𝐾)
3935, 38sseqtrrd 4018 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ ran 𝑓)
40 funimass1 6623 . . . . . . . . . . 11 ((Fun 𝑓𝑦 ⊆ ran 𝑓) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4132, 39, 40syl2anc 583 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓𝑦) ⊆ 𝑤𝑦 ⊆ (𝑓𝑤)))
4226, 41mpd 15 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑦 ⊆ (𝑓𝑤))
43 elssuni 4934 . . . . . . . . . . . 12 (𝑤𝐽𝑤 𝐽)
4443ad2antrl 725 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝑤 𝐽)
4527hmeocls 23622 . . . . . . . . . . 11 ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 𝐽) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
4622, 44, 45syl2anc 583 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤)))
47 simprrr 779 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥))
48 nrmtop 23190 . . . . . . . . . . . . . . 15 (𝐽 ∈ Nrm → 𝐽 ∈ Top)
4948ad3antrrr 727 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → 𝐽 ∈ Top)
5027clsss3 22913 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑤 𝐽) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
5149, 44, 50syl2anc 583 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ 𝐽)
52 f1odm 6830 . . . . . . . . . . . . . 14 (𝑓: 𝐽1-1-onto 𝐾 → dom 𝑓 = 𝐽)
5330, 52syl 17 . . . . . . . . . . . . 13 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → dom 𝑓 = 𝐽)
5451, 53sseqtrrd 4018 . . . . . . . . . . . 12 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓)
55 funimass3 7048 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5632, 54, 55syl2anc 583 . . . . . . . . . . 11 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))
5747, 56mpbird 257 . . . . . . . . . 10 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥)
5846, 57eqsstrd 4015 . . . . . . . . 9 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)
59 sseq2 4003 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (𝑦𝑧𝑦 ⊆ (𝑓𝑤)))
60 fveq2 6884 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓𝑤)))
6160sseq1d 4008 . . . . . . . . . . 11 (𝑧 = (𝑓𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥))
6259, 61anbi12d 630 . . . . . . . . . 10 (𝑧 = (𝑓𝑤) → ((𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)))
6362rspcev 3606 . . . . . . . . 9 (((𝑓𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓𝑤) ∧ ((cls‘𝐾)‘(𝑓𝑤)) ⊆ 𝑥)) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6425, 42, 58, 63syl12anc 834 . . . . . . . 8 ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤𝐽 ∧ ((𝑓𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑓𝑥)))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6521, 64rexlimddv 3155 . . . . . . 7 (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
6665ralrimivva 3194 . . . . . 6 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))
67 isnrm 23189 . . . . . 6 (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥𝐾𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧𝐾 (𝑦𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)))
686, 66, 67sylanbrc 582 . . . . 5 ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm)
6968expcom 413 . . . 4 (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
7069exlimiv 1925 . . 3 (∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
712, 70sylbi 216 . 2 ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
721, 71sylbi 216 1 (𝐽𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wex 1773  wcel 2098  wne 2934  wral 3055  wrex 3064  cin 3942  wss 3943  c0 4317  𝒫 cpw 4597   cuni 4902   class class class wbr 5141  ccnv 5668  dom cdm 5669  ran crn 5670  cima 5672  Fun wfun 6530  ontowfo 6534  1-1-ontowf1o 6535  cfv 6536  (class class class)co 7404  Topctop 22745  Clsdccld 22870  clsccl 22872   Cn ccn 23078  Nrmcnrm 23164  Homeochmeo 23607  chmph 23608
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7971  df-2nd 7972  df-1o 8464  df-map 8821  df-top 22746  df-topon 22763  df-cld 22873  df-cls 22875  df-cn 23081  df-nrm 23171  df-hmeo 23609  df-hmph 23610
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator