Proof of Theorem hmeores
Step | Hyp | Ref
| Expression |
1 | | hmeocn 21373 |
. . . . 5
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
3 | | hmeores.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
4 | 3 | cnrest 20899 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) |
5 | 2, 4 | sylancom 698 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾)) |
6 | | cntop2 20855 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
7 | 2, 6 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ Top) |
8 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
9 | 8 | toptopon 20548 |
. . . . 5
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
10 | 7, 9 | sylib 207 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
11 | | df-ima 5051 |
. . . . . 6
⊢ (𝐹 “ 𝑌) = ran (𝐹 ↾ 𝑌) |
12 | 11 | eqimss2i 3623 |
. . . . 5
⊢ ran
(𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌)) |
14 | | imassrn 5396 |
. . . . 5
⊢ (𝐹 “ 𝑌) ⊆ ran 𝐹 |
15 | 3, 8 | cnf 20860 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
16 | 2, 15 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) |
17 | | frn 5966 |
. . . . . 6
⊢ (𝐹:𝑋⟶∪ 𝐾 → ran 𝐹 ⊆ ∪ 𝐾) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) |
19 | 14, 18 | syl5ss 3579 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 “ 𝑌) ⊆ ∪ 𝐾) |
20 | | cnrest2 20900 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ran (𝐹 ↾ 𝑌) ⊆ (𝐹 “ 𝑌) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) |
21 | 10, 13, 19, 20 | syl3anc 1318 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn 𝐾) ↔ (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))))) |
22 | 5, 21 | mpbid 221 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌)))) |
23 | | hmeocnvcn 21374 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
25 | 8, 3 | cnf 20860 |
. . . . 5
⊢ (◡𝐹 ∈ (𝐾 Cn 𝐽) → ◡𝐹:∪ 𝐾⟶𝑋) |
26 | | ffun 5961 |
. . . . 5
⊢ (◡𝐹:∪ 𝐾⟶𝑋 → Fun ◡𝐹) |
27 | | funcnvres 5881 |
. . . . 5
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) |
28 | 24, 25, 26, 27 | 4syl 19 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) = (◡𝐹 ↾ (𝐹 “ 𝑌))) |
29 | 8 | cnrest 20899 |
. . . . 5
⊢ ((◡𝐹 ∈ (𝐾 Cn 𝐽) ∧ (𝐹 “ 𝑌) ⊆ ∪ 𝐾) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
30 | 24, 19, 29 | syl2anc 691 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡𝐹 ↾ (𝐹 “ 𝑌)) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
31 | 28, 30 | eqeltrd 2688 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽)) |
32 | | cntop1 20854 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
33 | 2, 32 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ Top) |
34 | 3 | toptopon 20548 |
. . . . 5
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
35 | 33, 34 | sylib 207 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
36 | | dfdm4 5238 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝑌) = ran ◡(𝐹 ↾ 𝑌) |
37 | | fssres 5983 |
. . . . . . . 8
⊢ ((𝐹:𝑋⟶∪ 𝐾 ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) |
38 | 16, 37 | sylancom 698 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾) |
39 | | fdm 5964 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝑌):𝑌⟶∪ 𝐾 → dom (𝐹 ↾ 𝑌) = 𝑌) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → dom (𝐹 ↾ 𝑌) = 𝑌) |
41 | 36, 40 | syl5eqr 2658 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) = 𝑌) |
42 | | eqimss 3620 |
. . . . 5
⊢ (ran
◡(𝐹 ↾ 𝑌) = 𝑌 → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) |
43 | 41, 42 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌) |
44 | | simpr 476 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ⊆ 𝑋) |
45 | | cnrest2 20900 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ran ◡(𝐹 ↾ 𝑌) ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
46 | 35, 43, 44, 45 | syl3anc 1318 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn 𝐽) ↔ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
47 | 31, 46 | mpbid 221 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌))) |
48 | | ishmeo 21372 |
. 2
⊢ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌))) ↔ ((𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌) Cn (𝐾 ↾t (𝐹 “ 𝑌))) ∧ ◡(𝐹 ↾ 𝑌) ∈ ((𝐾 ↾t (𝐹 “ 𝑌)) Cn (𝐽 ↾t 𝑌)))) |
49 | 22, 47, 48 | sylanbrc 695 |
1
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) |