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 ) )
3 2 adantr
 |-  ( ( 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 ) )
23 22 adantr
 |-  ( ( 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 ) ) ) )