This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrmhmph

Description: Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion nrmhmph ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Nrm → 𝐾 ∈ Nrm ) )

Proof

Step Hyp Ref Expression
1 hmph ⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
3 hmeocn ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
4 3 adantl ⊢ ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
5 cntop2 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
6 4 5 syl ⊢ ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐾 ∈ Top )
7 simpll ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝐽 ∈ Nrm )
8 4 adantr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
9 simprl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑥 ∈ 𝐾 )
10 cnima ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
12 simprr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) )
13 12 elin1d ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑦 ∈ ( Clsd ‘ 𝐾 ) )
14 cnclima ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝑓 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
15 8 13 14 syl2anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → ( ◡ 𝑓 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
16 12 elin2d ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑦 ∈ 𝒫 𝑥 )
17 16 elpwid ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → 𝑦 ⊆ 𝑥 )
18 imass2 ⊢ ( 𝑦 ⊆ 𝑥 → ( ◡ 𝑓 “ 𝑦 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) )
19 17 18 syl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → ( ◡ 𝑓 “ 𝑦 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) )
20 nrmsep3 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 ∧ ( ◡ 𝑓 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ 𝑓 “ 𝑦 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
21 7 11 15 19 20 syl13anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
22 simpllr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
23 simprl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑤 ∈ 𝐽 )
24 hmeoima ⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝑓 “ 𝑤 ) ∈ 𝐾 )
25 22 23 24 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( 𝑓 “ 𝑤 ) ∈ 𝐾 )
26 simprrl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 )
27 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
28 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
29 27 28 hmeof1o ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑓 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 )
30 22 29 syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑓 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 )
31 f1ofun ⊢ ( 𝑓 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → Fun 𝑓 )
32 30 31 syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → Fun 𝑓 )
33 13 adantr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑦 ∈ ( Clsd ‘ 𝐾 ) )
34 28 cldss ⊢ ( 𝑦 ∈ ( Clsd ‘ 𝐾 ) → 𝑦 ⊆ ∪ 𝐾 )
35 33 34 syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑦 ⊆ ∪ 𝐾 )
36 f1ofo ⊢ ( 𝑓 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → 𝑓 : ∪ 𝐽 –onto→ ∪ 𝐾 )
37 forn ⊢ ( 𝑓 : ∪ 𝐽 –onto→ ∪ 𝐾 → ran 𝑓 = ∪ 𝐾 )
38 30 36 37 3syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ran 𝑓 = ∪ 𝐾 )
39 35 38 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑦 ⊆ ran 𝑓 )
40 funimass1 ⊢ ( ( Fun 𝑓 ∧ 𝑦 ⊆ ran 𝑓 ) → ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 → 𝑦 ⊆ ( 𝑓 “ 𝑤 ) ) )
41 32 39 40 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 → 𝑦 ⊆ ( 𝑓 “ 𝑤 ) ) )
42 26 41 mpd ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑦 ⊆ ( 𝑓 “ 𝑤 ) )
43 elssuni ⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽 )
44 43 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝑤 ⊆ ∪ 𝐽 )
45 27 hmeocls ⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑤 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) = ( 𝑓 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
46 22 44 45 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) = ( 𝑓 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) )
47 simprrr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) )
48 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
49 48 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → 𝐽 ∈ Top )
50 27 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ∪ 𝐽 )
51 49 44 50 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ∪ 𝐽 )
52 f1odm ⊢ ( 𝑓 : ∪ 𝐽 –1-1-onto→ ∪ 𝐾 → dom 𝑓 = ∪ 𝐽 )
53 30 52 syl ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → dom 𝑓 = ∪ 𝐽 )
54 51 53 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ dom 𝑓 )
55 funimass3 ⊢ ( ( Fun 𝑓 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ dom 𝑓 ) → ( ( 𝑓 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
56 32 54 55 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( 𝑓 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) )
57 47 56 mpbird ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( 𝑓 “ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ) ⊆ 𝑥 )
58 46 57 eqsstrd ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) ⊆ 𝑥 )
59 sseq2 ⊢ ( 𝑧 = ( 𝑓 “ 𝑤 ) → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ( 𝑓 “ 𝑤 ) ) )
60 fveq2 ⊢ ( 𝑧 = ( 𝑓 “ 𝑤 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) = ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) )
61 60 sseq1d ⊢ ( 𝑧 = ( 𝑓 “ 𝑤 ) → ( ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) ⊆ 𝑥 ) )
62 59 61 anbi12d ⊢ ( 𝑧 = ( 𝑓 “ 𝑤 ) → ( ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) ↔ ( 𝑦 ⊆ ( 𝑓 “ 𝑤 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) ⊆ 𝑥 ) ) )
63 62 rspcev ⊢ ( ( ( 𝑓 “ 𝑤 ) ∈ 𝐾 ∧ ( 𝑦 ⊆ ( 𝑓 “ 𝑤 ) ∧ ( ( cls ‘ 𝐾 ) ‘ ( 𝑓 “ 𝑤 ) ) ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐾 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
64 25 42 58 63 syl12anc ⊢ ( ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝑓 “ 𝑦 ) ⊆ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( ◡ 𝑓 “ 𝑥 ) ) ) ) → ∃ 𝑧 ∈ 𝐾 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
65 21 64 rexlimddv ⊢ ( ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ) ) → ∃ 𝑧 ∈ 𝐾 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
66 65 ralrimivva ⊢ ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐾 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) )
67 isnrm ⊢ ( 𝐾 ∈ Nrm ↔ ( 𝐾 ∈ Top ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ ( ( Clsd ‘ 𝐾 ) ∩ 𝒫 𝑥 ) ∃ 𝑧 ∈ 𝐾 ( 𝑦 ⊆ 𝑧 ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑧 ) ⊆ 𝑥 ) ) )
68 6 66 67 sylanbrc ⊢ ( ( 𝐽 ∈ Nrm ∧ 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐾 ∈ Nrm )
69 68 expcom ⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝐽 ∈ Nrm → 𝐾 ∈ Nrm ) )
70 69 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ( 𝐽 ∈ Nrm → 𝐾 ∈ Nrm ) )
71 2 70 sylbi ⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ → ( 𝐽 ∈ Nrm → 𝐾 ∈ Nrm ) )
72 1 71 sylbi ⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Nrm → 𝐾 ∈ Nrm ) )