| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hmph 23785 | . 2
⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅) | 
| 2 |  | n0 4352 | . . 3
⊢ ((𝐽Homeo𝐾) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐽Homeo𝐾)) | 
| 3 |  | hmeocn 23769 | . . . . . . . 8
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 4 | 3 | adantl 481 | . . . . . . 7
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 5 |  | cntop2 23250 | . . . . . . 7
⊢ (𝑓 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Top) | 
| 7 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝐽 ∈ Nrm) | 
| 8 | 4 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 9 |  | simprl 770 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑥 ∈ 𝐾) | 
| 10 |  | cnima 23274 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝑓 “ 𝑥) ∈ 𝐽) | 
| 11 | 8, 9, 10 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑥) ∈ 𝐽) | 
| 12 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)) | 
| 13 | 12 | elin1d 4203 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ (Clsd‘𝐾)) | 
| 14 |  | cnclima 23277 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽)) | 
| 15 | 8, 13, 14 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽)) | 
| 16 | 12 | elin2d 4204 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ∈ 𝒫 𝑥) | 
| 17 | 16 | elpwid 4608 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → 𝑦 ⊆ 𝑥) | 
| 18 |  | imass2 6119 | . . . . . . . . . 10
⊢ (𝑦 ⊆ 𝑥 → (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥)) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . 9
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥)) | 
| 20 |  | nrmsep3 23364 | . . . . . . . . 9
⊢ ((𝐽 ∈ Nrm ∧ ((◡𝑓 “ 𝑥) ∈ 𝐽 ∧ (◡𝑓 “ 𝑦) ∈ (Clsd‘𝐽) ∧ (◡𝑓 “ 𝑦) ⊆ (◡𝑓 “ 𝑥))) → ∃𝑤 ∈ 𝐽 ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 21 | 7, 11, 15, 19, 20 | syl13anc 1373 | . . . . . . . 8
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑤 ∈ 𝐽 ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 22 |  | simpllr 775 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓 ∈ (𝐽Homeo𝐾)) | 
| 23 |  | simprl 770 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ∈ 𝐽) | 
| 24 |  | hmeoima 23774 | . . . . . . . . . 10
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ∈ 𝐽) → (𝑓 “ 𝑤) ∈ 𝐾) | 
| 25 | 22, 23, 24 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ 𝑤) ∈ 𝐾) | 
| 26 |  | simprrl 780 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (◡𝑓 “ 𝑦) ⊆ 𝑤) | 
| 27 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 28 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 29 | 27, 28 | hmeof1o 23773 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) | 
| 30 | 22, 29 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑓:∪ 𝐽–1-1-onto→∪ 𝐾) | 
| 31 |  | f1ofun 6849 | . . . . . . . . . . . 12
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ Fun 𝑓) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → Fun 𝑓) | 
| 33 | 13 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ∈ (Clsd‘𝐾)) | 
| 34 | 28 | cldss 23038 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (Clsd‘𝐾) → 𝑦 ⊆ ∪ 𝐾) | 
| 35 | 33, 34 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ∪ 𝐾) | 
| 36 |  | f1ofo 6854 | . . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝑓:∪ 𝐽–onto→∪ 𝐾) | 
| 37 |  | forn 6822 | . . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐽–onto→∪ 𝐾 → ran 𝑓 = ∪ 𝐾) | 
| 38 | 30, 36, 37 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ran 𝑓 = ∪ 𝐾) | 
| 39 | 35, 38 | sseqtrrd 4020 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ ran 𝑓) | 
| 40 |  | funimass1 6647 | . . . . . . . . . . 11
⊢ ((Fun
𝑓 ∧ 𝑦 ⊆ ran 𝑓) → ((◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤))) | 
| 41 | 32, 39, 40 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((◡𝑓 “ 𝑦) ⊆ 𝑤 → 𝑦 ⊆ (𝑓 “ 𝑤))) | 
| 42 | 26, 41 | mpd 15 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑦 ⊆ (𝑓 “ 𝑤)) | 
| 43 |  | elssuni 4936 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) | 
| 44 | 43 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝑤 ⊆ ∪ 𝐽) | 
| 45 | 27 | hmeocls 23777 | . . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝐽Homeo𝐾) ∧ 𝑤 ⊆ ∪ 𝐽) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) | 
| 46 | 22, 44, 45 | syl2anc 584 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) = (𝑓 “ ((cls‘𝐽)‘𝑤))) | 
| 47 |  | simprrr 781 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)) | 
| 48 |  | nrmtop 23345 | . . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ Nrm → 𝐽 ∈ Top) | 
| 49 | 48 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → 𝐽 ∈ Top) | 
| 50 | 27 | clsss3 23068 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑤 ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) | 
| 51 | 49, 44, 50 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ ∪ 𝐽) | 
| 52 |  | f1odm 6851 | . . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐽–1-1-onto→∪ 𝐾
→ dom 𝑓 = ∪ 𝐽) | 
| 53 | 30, 52 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → dom 𝑓 = ∪ 𝐽) | 
| 54 | 51, 53 | sseqtrrd 4020 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) | 
| 55 |  | funimass3 7073 | . . . . . . . . . . . 12
⊢ ((Fun
𝑓 ∧ ((cls‘𝐽)‘𝑤) ⊆ dom 𝑓) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 56 | 32, 54, 55 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥 ↔ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥))) | 
| 57 | 47, 56 | mpbird 257 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → (𝑓 “ ((cls‘𝐽)‘𝑤)) ⊆ 𝑥) | 
| 58 | 46, 57 | eqsstrd 4017 | . . . . . . . . 9
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥) | 
| 59 |  | sseq2 4009 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑓 “ 𝑤))) | 
| 60 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑓 “ 𝑤) → ((cls‘𝐾)‘𝑧) = ((cls‘𝐾)‘(𝑓 “ 𝑤))) | 
| 61 | 60 | sseq1d 4014 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑓 “ 𝑤) → (((cls‘𝐾)‘𝑧) ⊆ 𝑥 ↔ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) | 
| 62 | 59, 61 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = (𝑓 “ 𝑤) → ((𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥) ↔ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥))) | 
| 63 | 62 | rspcev 3621 | . . . . . . . . 9
⊢ (((𝑓 “ 𝑤) ∈ 𝐾 ∧ (𝑦 ⊆ (𝑓 “ 𝑤) ∧ ((cls‘𝐾)‘(𝑓 “ 𝑤)) ⊆ 𝑥)) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 64 | 25, 42, 58, 63 | syl12anc 836 | . . . . . . . 8
⊢ ((((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) ∧ (𝑤 ∈ 𝐽 ∧ ((◡𝑓 “ 𝑦) ⊆ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (◡𝑓 “ 𝑥)))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 65 | 21, 64 | rexlimddv 3160 | . . . . . . 7
⊢ (((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥))) → ∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 66 | 65 | ralrimivva 3201 | . . . . . 6
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥)) | 
| 67 |  | isnrm 23344 | . . . . . 6
⊢ (𝐾 ∈ Nrm ↔ (𝐾 ∈ Top ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ ((Clsd‘𝐾) ∩ 𝒫 𝑥)∃𝑧 ∈ 𝐾 (𝑦 ⊆ 𝑧 ∧ ((cls‘𝐾)‘𝑧) ⊆ 𝑥))) | 
| 68 | 6, 66, 67 | sylanbrc 583 | . . . . 5
⊢ ((𝐽 ∈ Nrm ∧ 𝑓 ∈ (𝐽Homeo𝐾)) → 𝐾 ∈ Nrm) | 
| 69 | 68 | expcom 413 | . . . 4
⊢ (𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | 
| 70 | 69 | exlimiv 1929 | . . 3
⊢
(∃𝑓 𝑓 ∈ (𝐽Homeo𝐾) → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | 
| 71 | 2, 70 | sylbi 217 | . 2
⊢ ((𝐽Homeo𝐾) ≠ ∅ → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | 
| 72 | 1, 71 | sylbi 217 | 1
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) |