| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hmph 23784 | . 2
⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅) | 
| 2 |  | n0 4353 | . . 3
⊢ ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾)) | 
| 3 |  | hmeocn 23768 | . . . . . . . 8
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 4 | 3 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 5 |  | cntop2 23249 | . . . . . . 7
⊢ (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top) | 
| 7 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝐽 ∈ Reg) | 
| 8 | 4 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 9 |  | simprl 771 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝐾) | 
| 10 |  | cnima 23273 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝑓 “ 𝑥) ∈ 𝐽) | 
| 11 | 8, 9, 10 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → (◡𝑓 “ 𝑥) ∈ 𝐽) | 
| 12 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 13 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 14 | 12, 13 | hmeof1o 23772 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) | 
| 15 | 14 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) | 
| 16 |  | f1ocnv 6860 | . . . . . . . . . . 11
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ ◡𝑓:∪ 𝐾–1-1-onto→∪ 𝐽) | 
| 17 |  | f1ofn 6849 | . . . . . . . . . . 11
⊢ (◡𝑓:∪ 𝐾–1-1-onto→∪ 𝐽
→ ◡𝑓 Fn ∪ 𝐾) | 
| 18 | 15, 16, 17 | 3syl 18 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → ◡𝑓 Fn ∪ 𝐾) | 
| 19 |  | elssuni 4937 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾) | 
| 20 | 19 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ⊆ ∪ 𝐾) | 
| 21 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) | 
| 22 |  | fnfvima 7253 | . . . . . . . . . 10
⊢ ((◡𝑓 Fn ∪ 𝐾 ∧ 𝑥 ⊆ ∪ 𝐾 ∧ 𝑦 ∈ 𝑥) → (◡𝑓‘𝑦) ∈ (◡𝑓 “ 𝑥)) | 
| 23 | 18, 20, 21, 22 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → (◡𝑓‘𝑦) ∈ (◡𝑓 “ 𝑥)) | 
| 24 |  | regsep 23342 | . . . . . . . . 9
⊢ ((𝐽 ∈ Reg ∧ (◡𝑓 “ 𝑥) ∈ 𝐽 ∧ (◡𝑓‘𝑦) ∈ (◡𝑓 “ 𝑥)) → ∃𝑤 ∈ 𝐽 ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 25 | 7, 11, 23, 24 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → ∃𝑤 ∈ 𝐽 ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 26 |  | simpllr 776 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾)) | 
| 27 |  | simprl 771 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ∈ 𝐽) | 
| 28 |  | hmeoima 23773 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ∈ 𝐽) → (𝑓 “ 𝑤) ∈ 𝐾) | 
| 29 | 26, 27, 28 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ 𝑤) ∈ 𝐾) | 
| 30 | 20, 21 | sseldd 3984 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ ∪ 𝐾) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ∈ ∪ 𝐾) | 
| 32 |  | simprrl 781 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (◡𝑓‘𝑦) ∈ 𝑤) | 
| 33 | 18 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ◡𝑓 Fn ∪ 𝐾) | 
| 34 |  | elpreima 7078 | . . . . . . . . . . . 12
⊢ (◡𝑓 Fn ∪ 𝐾 → (𝑦 ∈ (◡◡𝑓 “ 𝑤) ↔ (𝑦 ∈ ∪ 𝐾 ∧ (◡𝑓‘𝑦) ∈ 𝑤))) | 
| 35 | 33, 34 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑦 ∈ (◡◡𝑓 “ 𝑤) ↔ (𝑦 ∈ ∪ 𝐾 ∧ (◡𝑓‘𝑦) ∈ 𝑤))) | 
| 36 | 31, 32, 35 | mpbir2and 713 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ∈ (◡◡𝑓 “ 𝑤)) | 
| 37 |  | imacnvcnv 6226 | . . . . . . . . . 10
⊢ (◡◡𝑓 “ 𝑤) = (𝑓 “ 𝑤) | 
| 38 | 36, 37 | eleqtrdi 2851 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ∈ (𝑓 “ 𝑤)) | 
| 39 |  | elssuni 4937 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) | 
| 40 | 39 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ⊆ ∪ 𝐽) | 
| 41 | 12 | hmeocls 23776 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) | 
| 42 | 26, 40, 41 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) | 
| 43 |  | simprrr 782 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)) | 
| 44 | 15 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) | 
| 45 |  | f1ofun 6850 | . . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ Fun 𝑓) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → Fun 𝑓) | 
| 47 | 7 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝐽 ∈ Reg) | 
| 48 |  | regtop 23341 | . . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Reg → 𝐽 ∈ Top) | 
| 49 | 47, 48 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝐽 ∈ Top) | 
| 50 | 12 | clsss3 23067 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) | 
| 51 | 49, 40, 50 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) | 
| 52 |  | f1odm 6852 | . . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ dom 𝑓 = ∪ 𝐽) | 
| 53 | 44, 52 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → dom 𝑓 = ∪ 𝐽) | 
| 54 | 51, 53 | sseqtrrd 4021 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) | 
| 55 |  | funimass3 7074 | . . . . . . . . . . . 12
⊢ ((Fun
𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 56 | 46, 54, 55 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 57 | 43, 56 | mpbird 257 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥) | 
| 58 | 42, 57 | eqsstrd 4018 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥) | 
| 59 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ (𝑓 “ 𝑤))) | 
| 60 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑓 “ 𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓 “ 𝑤))) | 
| 61 | 60 | sseq1d 4015 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) | 
| 62 | 59, 61 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = (𝑓 “ 𝑤) → ((𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ∈ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥))) | 
| 63 | 62 | rspcev 3622 | . . . . . . . . 9
⊢ (((𝑓 “ 𝑤) ∈ 𝐾 ∧ (𝑦 ∈ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) → ∃𝑧 ∈ 𝐾 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 64 | 29, 38, 58, 63 | syl12anc 837 | . . . . . . . 8
⊢ ((((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓‘𝑦) ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ∃𝑧 ∈ 𝐾 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 65 | 25, 64 | rexlimddv 3161 | . . . . . . 7
⊢ (((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑥)) → ∃𝑧 ∈ 𝐾 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 66 | 65 | ralrimivva 3202 | . . . . . 6
⊢ ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐾 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 67 |  | isreg 23340 | . . . . . 6
⊢ (𝐾 ∈ Reg ↔ (𝐾 ∈ Top ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐾 (𝑦 ∈ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))) | 
| 68 | 6, 66, 67 | sylanbrc 583 | . . . . 5
⊢ ((𝐽 ∈ Reg ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Reg) | 
| 69 | 68 | expcom 413 | . . . 4
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | 
| 70 | 69 | exlimiv 1930 | . . 3
⊢
(∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | 
| 71 | 2, 70 | sylbi 217 | . 2
⊢ ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | 
| 72 | 1, 71 | sylbi 217 | 1
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) |