| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cmphaushmeo.1 | . . 3
⊢ 𝑋 = ∪
𝐽 | 
| 2 |  | cmphaushmeo.2 | . . 3
⊢ 𝑌 = ∪
𝐾 | 
| 3 | 1, 2 | hmeof1o 23773 | . 2
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) | 
| 4 |  | f1ocnv 6859 | . . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) | 
| 5 |  | f1of 6847 | . . . . . . . 8
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) | 
| 6 | 4, 5 | syl 17 | . . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋) | 
| 7 | 6 | a1i 11 | . . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌⟶𝑋)) | 
| 8 |  | f1orel 6850 | . . . . . . . . . . . 12
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Rel 𝐹) | 
| 9 | 8 | ad2antll 729 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → Rel 𝐹) | 
| 10 |  | dfrel2 6208 | . . . . . . . . . . 11
⊢ (Rel
𝐹 ↔ ◡◡𝐹 = 𝐹) | 
| 11 | 9, 10 | sylib 218 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → ◡◡𝐹 = 𝐹) | 
| 12 | 11 | imaeq1d 6076 | . . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (◡◡𝐹 “ 𝑥) = (𝐹 “ 𝑥)) | 
| 13 |  | simp2 1137 | . . . . . . . . . . 11
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus) | 
| 14 | 13 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐾 ∈ Haus) | 
| 15 |  | imassrn 6088 | . . . . . . . . . . 11
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 | 
| 16 |  | f1ofo 6854 | . . . . . . . . . . . . 13
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) | 
| 17 | 16 | ad2antll 729 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐹:𝑋–onto→𝑌) | 
| 18 |  | forn 6822 | . . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → ran 𝐹 = 𝑌) | 
| 20 | 15, 19 | sseqtrid 4025 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐹 “ 𝑥) ⊆ 𝑌) | 
| 21 |  | simpl3 1193 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 22 |  | simp1 1136 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Comp) | 
| 23 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝐽 ∈ Comp) | 
| 24 |  | simprl 770 | . . . . . . . . . . . 12
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → 𝑥 ∈ (Clsd‘𝐽)) | 
| 25 |  | cmpcld 23411 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Comp ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑥) ∈ Comp) | 
| 26 | 23, 24, 25 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐽 ↾t 𝑥) ∈ Comp) | 
| 27 |  | imacmp 23406 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐽 ↾t 𝑥) ∈ Comp) → (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) | 
| 28 | 21, 26, 27 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) | 
| 29 | 2 | hauscmp 23416 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Haus ∧ (𝐹 “ 𝑥) ⊆ 𝑌 ∧ (𝐾 ↾t (𝐹 “ 𝑥)) ∈ Comp) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) | 
| 30 | 14, 20, 28, 29 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) | 
| 31 | 12, 30 | eqeltrd 2840 | . . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝐹:𝑋–1-1-onto→𝑌)) → (◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) | 
| 32 | 31 | expr 456 | . . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹:𝑋–1-1-onto→𝑌 → (◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾))) | 
| 33 | 32 | ralrimdva 3153 | . . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾))) | 
| 34 | 7, 33 | jcad 512 | . . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) | 
| 35 |  | haustop 23340 | . . . . . . . 8
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) | 
| 36 | 13, 35 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) | 
| 37 | 2 | toptopon 22924 | . . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) | 
| 38 | 36, 37 | sylib 218 | . . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘𝑌)) | 
| 39 |  | cmptop 23404 | . . . . . . . 8
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) | 
| 40 | 22, 39 | syl 17 | . . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top) | 
| 41 | 1 | toptopon 22924 | . . . . . . 7
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) | 
| 42 | 40, 41 | sylib 218 | . . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 43 |  | iscncl 23278 | . . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐽 ∈ (TopOn‘𝑋)) → (◡𝐹 ∈ (𝐾 Cn 𝐽) ↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) | 
| 44 | 38, 42, 43 | syl2anc 584 | . . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (◡𝐹 ∈ (𝐾 Cn 𝐽) ↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡◡𝐹 “ 𝑥) ∈ (Clsd‘𝐾)))) | 
| 45 | 34, 44 | sylibrd 259 | . . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹 ∈ (𝐾 Cn 𝐽))) | 
| 46 |  | simp3 1138 | . . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 47 | 45, 46 | jctild 525 | . . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽)))) | 
| 48 |  | ishmeo 23768 | . . 3
⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) | 
| 49 | 47, 48 | imbitrrdi 252 | . 2
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 ∈ (𝐽Homeo𝐾))) | 
| 50 | 3, 49 | impbid2 226 | 1
⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹:𝑋–1-1-onto→𝑌)) |