# 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
`|- X = U. J`
Assertion hmeores
`|- ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J |`t Y ) Homeo ( K |`t ( F " Y ) ) ) )`

### Proof

Step Hyp Ref Expression
1 hmeores.1
` |-  X = U. J`
2 hmeocn
` |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )`
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> F e. ( J Cn K ) )`
4 1 cnrest
` |-  ( ( F e. ( J Cn K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J |`t Y ) Cn K ) )`
5 3 4 sylancom
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J |`t Y ) Cn K ) )`
6 cntop2
` |-  ( F e. ( J Cn K ) -> K e. Top )`
7 3 6 syl
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> K e. Top )`
8 eqid
` |-  U. K = U. K`
9 8 toptopon
` |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )`
10 7 9 sylib
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> K e. ( TopOn ` U. K ) )`
11 df-ima
` |-  ( F " Y ) = ran ( F |` Y )`
12 11 eqimss2i
` |-  ran ( F |` Y ) C_ ( F " Y )`
13 12 a1i
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ran ( F |` Y ) C_ ( F " Y ) )`
14 imassrn
` |-  ( F " Y ) C_ ran F`
15 1 8 cnf
` |-  ( F e. ( J Cn K ) -> F : X --> U. K )`
16 3 15 syl
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> F : X --> U. K )`
17 16 frnd
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ran F C_ U. K )`
18 14 17 sstrid
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F " Y ) C_ U. K )`
19 cnrest2
` |-  ( ( K e. ( TopOn ` U. K ) /\ ran ( F |` Y ) C_ ( F " Y ) /\ ( F " Y ) C_ U. K ) -> ( ( F |` Y ) e. ( ( J |`t Y ) Cn K ) <-> ( F |` Y ) e. ( ( J |`t Y ) Cn ( K |`t ( F " Y ) ) ) ) )`
20 10 13 18 19 syl3anc
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( ( F |` Y ) e. ( ( J |`t Y ) Cn K ) <-> ( F |` Y ) e. ( ( J |`t Y ) Cn ( K |`t ( F " Y ) ) ) ) )`
21 5 20 mpbid
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J |`t Y ) Cn ( K |`t ( F " Y ) ) ) )`
22 hmeocnvcn
` |-  ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )`
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> `' F e. ( K Cn J ) )`
24 8 1 cnf
` |-  ( `' F e. ( K Cn J ) -> `' F : U. K --> X )`
25 ffun
` |-  ( `' F : U. K --> X -> Fun `' F )`
26 funcnvres
` |-  ( Fun `' F -> `' ( F |` Y ) = ( `' F |` ( F " Y ) ) )`
27 23 24 25 26 4syl
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> `' ( F |` Y ) = ( `' F |` ( F " Y ) ) )`
28 8 cnrest
` |-  ( ( `' F e. ( K Cn J ) /\ ( F " Y ) C_ U. K ) -> ( `' F |` ( F " Y ) ) e. ( ( K |`t ( F " Y ) ) Cn J ) )`
29 23 18 28 syl2anc
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( `' F |` ( F " Y ) ) e. ( ( K |`t ( F " Y ) ) Cn J ) )`
30 27 29 eqeltrd
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn J ) )`
31 cntop1
` |-  ( F e. ( J Cn K ) -> J e. Top )`
32 3 31 syl
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> J e. Top )`
33 1 toptopon
` |-  ( J e. Top <-> J e. ( TopOn ` X ) )`
34 32 33 sylib
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> J e. ( TopOn ` X ) )`
35 dfdm4
` |-  dom ( F |` Y ) = ran `' ( F |` Y )`
36 fssres
` |-  ( ( F : X --> U. K /\ Y C_ X ) -> ( F |` Y ) : Y --> U. K )`
37 16 36 sylancom
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) : Y --> U. K )`
38 37 fdmd
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> dom ( F |` Y ) = Y )`
39 35 38 syl5eqr
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ran `' ( F |` Y ) = Y )`
40 eqimss
` |-  ( ran `' ( F |` Y ) = Y -> ran `' ( F |` Y ) C_ Y )`
41 39 40 syl
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ran `' ( F |` Y ) C_ Y )`
42 simpr
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> Y C_ X )`
43 cnrest2
` |-  ( ( J e. ( TopOn ` X ) /\ ran `' ( F |` Y ) C_ Y /\ Y C_ X ) -> ( `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn J ) <-> `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn ( J |`t Y ) ) ) )`
44 34 41 42 43 syl3anc
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn J ) <-> `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn ( J |`t Y ) ) ) )`
45 30 44 mpbid
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn ( J |`t Y ) ) )`
46 ishmeo
` |-  ( ( F |` Y ) e. ( ( J |`t Y ) Homeo ( K |`t ( F " Y ) ) ) <-> ( ( F |` Y ) e. ( ( J |`t Y ) Cn ( K |`t ( F " Y ) ) ) /\ `' ( F |` Y ) e. ( ( K |`t ( F " Y ) ) Cn ( J |`t Y ) ) ) )`
47 21 45 46 sylanbrc
` |-  ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J |`t Y ) Homeo ( K |`t ( F " Y ) ) ) )`