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 \in (J Homeo K) \land Y \subseteq X) \to {F ↾}_{Y} \in ((J ↾_{𝑡} Y) Homeo (K ↾_{𝑡} F [Y]))$

Proof

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

Metamath Proof Explorer

Theorem hmeores

Proof