Theorem cncfmptss

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	cncfmptss.1	$$⊢\underset{\_}{Ⅎ}xF$$
	cncfmptss.2	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
	cncfmptss.3	$$⊢\phi \to C\subseteq A$$
Assertion	cncfmptss	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right):C\underset{cn}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		cncfmptss.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		cncfmptss.2	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
3		cncfmptss.3	$$⊢\phi \to C\subseteq A$$
4	3	resmptd	$$⊢\phi \to {\left(y\in A⟼F\left(y\right)\right)\upharpoonright }_C=\left(y\in C⟼F\left(y\right)\right)$$
5		cncff	$$⊢F:A\underset{cn}{⟶}B\to F:A⟶B$$
6	2 5	syl	$$⊢\phi \to F:A⟶B$$
7	6	feqmptd	$$⊢\phi \to F=\left(y\in A⟼F\left(y\right)\right)$$
8	7	reseq1d	$$⊢\phi \to {F\upharpoonright }_C={\left(y\in A⟼F\left(y\right)\right)\upharpoonright }_C$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}yF$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yx$$
11	9 10	nffv	$$⊢\underset{\_}{Ⅎ}yF\left(x\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
14		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
15	11 13 14	cbvmpt	$$⊢\left(x\in C⟼F\left(x\right)\right)=\left(y\in C⟼F\left(y\right)\right)$$
16	15	a1i	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right)=\left(y\in C⟼F\left(y\right)\right)$$
17	4 8 16	3eqtr4rd	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right)={F\upharpoonright }_C$$
18		rescncf	$$⊢C\subseteq A\to \left(F:A\underset{cn}{⟶}B\to \left({F\upharpoonright }_C\right):C\underset{cn}{⟶}B\right)$$
19	3 2 18	sylc	$$⊢\phi \to \left({F\upharpoonright }_C\right):C\underset{cn}{⟶}B$$
20	17 19	eqeltrd	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right):C\underset{cn}{⟶}B$$