Proof of Theorem hmeores
Step | Hyp | Ref
| Expression |
1 | | hmeocn 13064 |
. . . . 5
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | 1 | adantr 274 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
3 | | hmeores.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
4 | 3 | cnrest 12994 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) |
5 | 2, 4 | sylancom 418 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) |
6 | | cntop2 12961 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
7 | 2, 6 | syl 14 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ Top) |
8 | | eqid 2170 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
9 | 8 | toptopon 12775 |
. . . . 5
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
10 | 7, 9 | sylib 121 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | | df-ima 4622 |
. . . . . 6
⊢ (𝐹 “ 𝑌) = ran (𝐹 ↾ 𝑌) |
12 | 11 | eqimss2i 3204 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) |
13 | 12 | a1i 9 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌)) |
14 | | imassrn 4962 |
. . . . 5
⊢ (𝐹 “ 𝑌) ⊆ ran 𝐹 |
15 | 3, 8 | cnf 12963 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
16 | 2, 15 | syl 14 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) |
17 | 16 | frnd 5355 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) |
18 | 14, 17 | sstrid 3158 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 “ 𝑌) ⊆ ∪ 𝐾) |
19 | | cnrest2 12995 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) |
20 | 10, 13, 18, 19 | syl3anc 1233 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) |
21 | 5, 20 | mpbid 146 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌)))) |
22 | | hmeocnvcn 13065 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
23 | 22 | adantr 274 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
24 | 8, 3 | cnf 12963 |
. . . . 5
⊢ (◡𝐹 ∈ (𝐾 Cn 𝐽) → ◡𝐹:∪ 𝐾⟶𝑋) |
25 | | ffun 5348 |
. . . . 5
⊢ (◡𝐹:∪ 𝐾⟶𝑋 → Fun ◡𝐹) |
26 | | funcnvres 5269 |
. . . . 5
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) |
27 | 23, 24, 25, 26 | 4syl 18 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) |
28 | 8 | cnrest 12994 |
. . . . 5
⊢ ((◡𝐹 ∈ (𝐾 Cn 𝐽) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
29 | 23, 18, 28 | syl2anc 409 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
30 | 27, 29 | eqeltrd 2247 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
31 | | cntop1 12960 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
32 | 2, 31 | syl 14 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ Top) |
33 | 3 | toptopon 12775 |
. . . . 5
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
34 | 32, 33 | sylib 121 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
35 | | dfdm4 4801 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝑌) = ran ◡(𝐹 ↾ 𝑌) |
36 | | fssres 5371 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶∪ 𝐾 ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) |
37 | 16, 36 | sylancom 418 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) |
38 | 37 | fdmd 5352 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → dom (𝐹 ↾ 𝑌) = 𝑌) |
39 | 35, 38 | eqtr3id 2217 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) = 𝑌) |
40 | | eqimss 3201 |
. . . . 5
⊢ (ran
◡(𝐹 ↾ 𝑌) = 𝑌 → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) |
41 | 39, 40 | syl 14 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) |
42 | | simpr 109 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ⊆ 𝑋) |
43 | | cnrest2 12995 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
44 | 34, 41, 42, 43 | syl3anc 1233 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
45 | 30, 44 | mpbid 146 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌))) |
46 | | ishmeo 13063 |
. 2
⊢ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌))) ↔ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))) ∧ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
47 | 21, 45, 46 | sylanbrc 415 |
1
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) |