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 = J
Assertion hmeores F J Homeo K Y X F Y J 𝑡 Y Homeo K 𝑡 F Y

Proof

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