Theorem cncfmptssg

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfmptssg.2	$$⊢F=\left(x\in A⟼E\right)$$
	cncfmptssg.3	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
	cncfmptssg.4	$$⊢\phi \to C\subseteq A$$
	cncfmptssg.5	$$⊢\phi \to D\subseteq B$$
	cncfmptssg.6	$$⊢\left(\phi \wedge x\in C\right)\to E\in D$$
Assertion	cncfmptssg	$$⊢\phi \to \left(x\in C⟼E\right):C\underset{cn}{⟶}D$$

Proof

Step	Hyp	Ref	Expression
1		cncfmptssg.2	$$⊢F=\left(x\in A⟼E\right)$$
2		cncfmptssg.3	$$⊢\phi \to F:A\underset{cn}{⟶}B$$
3		cncfmptssg.4	$$⊢\phi \to C\subseteq A$$
4		cncfmptssg.5	$$⊢\phi \to D\subseteq B$$
5		cncfmptssg.6	$$⊢\left(\phi \wedge x\in C\right)\to E\in D$$
6	5	fmpttd	$$⊢\phi \to \left(x\in C⟼E\right):C⟶D$$
7		cncfrss2	$$⊢F:A\underset{cn}{⟶}B\to B\subseteq ℂ$$
8	2 7	syl	$$⊢\phi \to B\subseteq ℂ$$
9	4 8	sstrd	$$⊢\phi \to D\subseteq ℂ$$
10	3	sselda	$$⊢\left(\phi \wedge x\in C\right)\to x\in A$$
11	1	fvmpt2	$$⊢\left(x\in A\wedge E\in D\right)\to F\left(x\right)=E$$
12	10 5 11	syl2anc	$$⊢\left(\phi \wedge x\in C\right)\to F\left(x\right)=E$$
13	12	mpteq2dva	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right)=\left(x\in C⟼E\right)$$
14		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼E\right)$$
15	1 14	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
16	15 2 3	cncfmptss	$$⊢\phi \to \left(x\in C⟼F\left(x\right)\right):C\underset{cn}{⟶}B$$
17	13 16	eqeltrrd	$$⊢\phi \to \left(x\in C⟼E\right):C\underset{cn}{⟶}B$$
18		cncffvrn	$$⊢\left(D\subseteq ℂ\wedge \left(x\in C⟼E\right):C\underset{cn}{⟶}B\right)\to \left(\left(x\in C⟼E\right):C\underset{cn}{⟶}D\leftrightarrow \left(x\in C⟼E\right):C⟶D\right)$$
19	9 17 18	syl2anc	$$⊢\phi \to \left(\left(x\in C⟼E\right):C\underset{cn}{⟶}D\leftrightarrow \left(x\in C⟼E\right):C⟶D\right)$$
20	6 19	mpbird	$$⊢\phi \to \left(x\in C⟼E\right):C\underset{cn}{⟶}D$$