Theorem cnmpt1res

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	cnmpt1res.2	$$⊢K=J{\upharpoonright }_{𝑡}Y$$
	cnmpt1res.3	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	cnmpt1res.5	$$⊢\phi \to Y\subseteq X$$
	cnmpt1res.6	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(J\mathrm{Cn}L\right)$$
Assertion	cnmpt1res	$$⊢\phi \to \left(x\in Y⟼A\right)\in \left(K\mathrm{Cn}L\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmpt1res.2	$$⊢K=J{\upharpoonright }_{𝑡}Y$$
2		cnmpt1res.3	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
3		cnmpt1res.5	$$⊢\phi \to Y\subseteq X$$
4		cnmpt1res.6	$$⊢\phi \to \left(x\in X⟼A\right)\in \left(J\mathrm{Cn}L\right)$$
5	3	resmptd	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_Y=\left(x\in Y⟼A\right)$$
6		toponuni	$$⊢J\in \mathrm{TopOn}\left(X\right)\to X=\bigcup J$$
7	2 6	syl	$$⊢\phi \to X=\bigcup J$$
8	3 7	sseqtrd	$$⊢\phi \to Y\subseteq \bigcup J$$
9		eqid	$$⊢\bigcup J=\bigcup J$$
10	9	cnrest	$$⊢\left(\left(x\in X⟼A\right)\in \left(J\mathrm{Cn}L\right)\wedge Y\subseteq \bigcup J\right)\to {\left(x\in X⟼A\right)\upharpoonright }_Y\in \left(\left(J{\upharpoonright }_{𝑡}Y\right)\mathrm{Cn}L\right)$$
11	4 8 10	syl2anc	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_Y\in \left(\left(J{\upharpoonright }_{𝑡}Y\right)\mathrm{Cn}L\right)$$
12	1	oveq1i	$$⊢K\mathrm{Cn}L=\left(J{\upharpoonright }_{𝑡}Y\right)\mathrm{Cn}L$$
13	11 12	eleqtrrdi	$$⊢\phi \to {\left(x\in X⟼A\right)\upharpoonright }_Y\in \left(K\mathrm{Cn}L\right)$$
14	5 13	eqeltrrd	$$⊢\phi \to \left(x\in Y⟼A\right)\in \left(K\mathrm{Cn}L\right)$$