Metamath Proof Explorer

Theorem reghmph

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

Ref Expression
Assertion reghmph ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Reg → 𝐾 ∈ Reg ) )

Proof

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