Metamath Proof Explorer

Theorem hmeores

Description: The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis hmeores.1 ⊢ 𝑋 = ∪ 𝐽
Assertion hmeores ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Homeo ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 hmeores.1 ⊢ 𝑋 = ∪ 𝐽
2 hmeocn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
4 1 cnrest ⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
5 3 4 sylancom ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
6 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
7 3 6 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ Top )
8 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
9 8 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
10 7 9 sylib ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
11 df-ima ⊢ ( 𝐹 “ 𝑌 ) = ran ( 𝐹 ↾ 𝑌 )
12 11 eqimss2i ⊢ ran ( 𝐹 ↾ 𝑌 ) ⊆ ( 𝐹 “ 𝑌 )
13 12 a1i ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ran ( 𝐹 ↾ 𝑌 ) ⊆ ( 𝐹 “ 𝑌 ) )
14 imassrn ⊢ ( 𝐹 “ 𝑌 ) ⊆ ran 𝐹
15 1 8 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
16 3 15 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 )
17 16 frnd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ran 𝐹 ⊆ ∪ 𝐾 )
18 14 17 sstrid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 “ 𝑌 ) ⊆ ∪ 𝐾 )
19 cnrest2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ran ( 𝐹 ↾ 𝑌 ) ⊆ ( 𝐹 “ 𝑌 ) ∧ ( 𝐹 “ 𝑌 ) ⊆ ∪ 𝐾 ) → ( ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) ) )
20 10 13 18 19 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ↔ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) ) )
21 5 20 mpbid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) )
22 hmeocnvcn ⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
24 8 1 cnf ⊢ ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) → ◡ 𝐹 : ∪ 𝐾 ⟶ 𝑋 )
25 ffun ⊢ ( ◡ 𝐹 : ∪ 𝐾 ⟶ 𝑋 → Fun ◡ 𝐹 )
26 funcnvres ⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝑌 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑌 ) ) )
27 23 24 25 26 4syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ◡ ( 𝐹 ↾ 𝑌 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑌 ) ) )
28 8 cnrest ⊢ ( ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ ( 𝐹 “ 𝑌 ) ⊆ ∪ 𝐾 ) → ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑌 ) ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn 𝐽 ) )
29 23 18 28 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑌 ) ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn 𝐽 ) )
30 27 29 eqeltrd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn 𝐽 ) )
31 cntop1 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
32 3 31 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐽 ∈ Top )
33 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
34 32 33 sylib ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
35 dfdm4 ⊢ dom ( 𝐹 ↾ 𝑌 ) = ran ◡ ( 𝐹 ↾ 𝑌 )
36 fssres ⊢ ( ( 𝐹 : 𝑋 ⟶ ∪ 𝐾 ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) : 𝑌 ⟶ ∪ 𝐾 )
37 16 36 sylancom ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) : 𝑌 ⟶ ∪ 𝐾 )
38 37 fdmd ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → dom ( 𝐹 ↾ 𝑌 ) = 𝑌 )
39 35 38 eqtr3id ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ran ◡ ( 𝐹 ↾ 𝑌 ) = 𝑌 )
40 eqimss ⊢ ( ran ◡ ( 𝐹 ↾ 𝑌 ) = 𝑌 → ran ◡ ( 𝐹 ↾ 𝑌 ) ⊆ 𝑌 )
41 39 40 syl ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ran ◡ ( 𝐹 ↾ 𝑌 ) ⊆ 𝑌 )
42 simpr ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ⊆ 𝑋 )
43 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ran ◡ ( 𝐹 ↾ 𝑌 ) ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋 ) → ( ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn 𝐽 ) ↔ ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn ( 𝐽 ↾t 𝑌 ) ) ) )
44 34 41 42 43 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn 𝐽 ) ↔ ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn ( 𝐽 ↾t 𝑌 ) ) ) )
45 30 44 mpbid ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn ( 𝐽 ↾t 𝑌 ) ) )
46 ishmeo ⊢ ( ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Homeo ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) ↔ ( ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Cn ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) ∧ ◡ ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) Cn ( 𝐽 ↾t 𝑌 ) ) ) )
47 21 45 46 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝑌 ) ∈ ( ( 𝐽 ↾t 𝑌 ) Homeo ( 𝐾 ↾t ( 𝐹 “ 𝑌 ) ) ) )