Proof of Theorem hmeores
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hmeocn 23769 | . . . . 5
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 3 |  | hmeores.1 | . . . . 5
⊢ 𝑋 = ∪
𝐽 | 
| 4 | 3 | cnrest 23294 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) | 
| 5 | 2, 4 | sylancom 588 | . . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) | 
| 6 |  | cntop2 23250 | . . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | 
| 7 | 2, 6 | syl 17 | . . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ Top) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 9 | 8 | toptopon 22924 | . . . . 5
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 10 | 7, 9 | sylib 218 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 11 |  | df-ima 5697 | . . . . . 6
⊢ (𝐹 “ 𝑌) = ran (𝐹 ↾ 𝑌) | 
| 12 | 11 | eqimss2i 4044 | . . . . 5
⊢ ran
(𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) | 
| 13 | 12 | a1i 11 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌)) | 
| 14 |  | imassrn 6088 | . . . . 5
⊢ (𝐹 “ 𝑌) ⊆ ran 𝐹 | 
| 15 | 3, 8 | cnf 23255 | . . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) | 
| 16 | 2, 15 | syl 17 | . . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) | 
| 17 | 16 | frnd 6743 | . . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) | 
| 18 | 14, 17 | sstrid 3994 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 “ 𝑌) ⊆ ∪ 𝐾) | 
| 19 |  | cnrest2 23295 | . . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) | 
| 20 | 10, 13, 18, 19 | syl3anc 1372 | . . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) | 
| 21 | 5, 20 | mpbid 232 | . 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌)))) | 
| 22 |  | hmeocnvcn 23770 | . . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) | 
| 24 | 8, 3 | cnf 23255 | . . . . 5
⊢ (◡𝐹 ∈ (𝐾 Cn 𝐽) → ◡𝐹:∪ 𝐾⟶𝑋) | 
| 25 |  | ffun 6738 | . . . . 5
⊢ (◡𝐹:∪ 𝐾⟶𝑋 → Fun ◡𝐹) | 
| 26 |  | funcnvres 6643 | . . . . 5
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) | 
| 27 | 23, 24, 25, 26 | 4syl 19 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) | 
| 28 | 8 | cnrest 23294 | . . . . 5
⊢ ((◡𝐹 ∈ (𝐾 Cn 𝐽) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) | 
| 29 | 23, 18, 28 | syl2anc 584 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) | 
| 30 | 27, 29 | eqeltrd 2840 | . . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) | 
| 31 |  | cntop1 23249 | . . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | 
| 32 | 2, 31 | syl 17 | . . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ Top) | 
| 33 | 3 | toptopon 22924 | . . . . 5
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) | 
| 34 | 32, 33 | sylib 218 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 35 |  | dfdm4 5905 | . . . . . 6
⊢ dom
(𝐹 ↾ 𝑌) = ran ◡(𝐹 ↾ 𝑌) | 
| 36 |  | fssres 6773 | . . . . . . . 8
⊢ ((𝐹:𝑋⟶∪ 𝐾 ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) | 
| 37 | 16, 36 | sylancom 588 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) | 
| 38 | 37 | fdmd 6745 | . . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → dom (𝐹 ↾ 𝑌) = 𝑌) | 
| 39 | 35, 38 | eqtr3id 2790 | . . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) = 𝑌) | 
| 40 |  | eqimss 4041 | . . . . 5
⊢ (ran
◡(𝐹 ↾ 𝑌) = 𝑌 → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) | 
| 41 | 39, 40 | syl 17 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) | 
| 42 |  | simpr 484 | . . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ⊆ 𝑋) | 
| 43 |  | cnrest2 23295 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) | 
| 44 | 34, 41, 42, 43 | syl3anc 1372 | . . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) | 
| 45 | 30, 44 | mpbid 232 | . 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌))) | 
| 46 |  | ishmeo 23768 | . 2
⊢ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌))) ↔ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))) ∧ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) | 
| 47 | 21, 45, 46 | sylanbrc 583 | 1
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) |