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 eqtr3id 
 |-  ( ( 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 ) ) ) )