cnres2

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Hypotheses	cnres2.1	$⊢ X = ⋃ J$
	cnres2.2	$⊢ Y = ⋃ K$
Assertion	cnres2	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} B))$

Proof

Step	Hyp	Ref	Expression
1		cnres2.1	$⊢ X = ⋃ J$
2		cnres2.2	$⊢ Y = ⋃ K$
3		simp3l	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to F \in (J Cn K)$
4		simp2l	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to A \subseteq X$
5	1	cnrest	$⊢ (F \in (J Cn K) \land A \subseteq X) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
6	3 4 5	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
7		simp1r	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to K \in Top$
8	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
9	7 8	sylib	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to K \in TopOn (Y)$
10		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
11		simp3r	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to \forall x \in A F (x) \in B$
12	1 2	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ Y$
13		ffun	$⊢ F : X ⟶ Y \to Fun F$
14	3 12 13	3syl	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to Fun F$
15		fdm	$⊢ F : X ⟶ Y \to dom F = X$
16	3 12 15	3syl	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to dom F = X$
17	4 16	sseqtrrd	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to A \subseteq dom F$
18		funimass4	$⊢ (Fun F \land A \subseteq dom F) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$
19	14 17 18	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to (F [A] \subseteq B \leftrightarrow \forall x \in A F (x) \in B)$
20	11 19	mpbird	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to F [A] \subseteq B$
21	10 20	eqsstrrid	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to ran ({F ↾}_{A}) \subseteq B$
22		simp2r	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to B \subseteq Y$
23		cnrest2	$⊢ (K \in TopOn (Y) \land ran ({F ↾}_{A}) \subseteq B \land B \subseteq Y) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} B)))$
24	9 21 22 23	syl3anc	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} B)))$
25	6 24	mpbid	$⊢ ((J \in Top \land K \in Top) \land (A \subseteq X \land B \subseteq Y) \land (F \in (J Cn K) \land \forall x \in A F (x) \in B)) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn (K ↾_{𝑡} B))$

Metamath Proof Explorer

Theorem cnres2

Proof