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	⊢ Ⅎ 𝑥 𝐹
	cncfmptss.2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
	cncfmptss.3	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion	cncfmptss	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmptss.1	⊢ Ⅎ 𝑥 𝐹
2		cncfmptss.2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
3		cncfmptss.3	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4	3	resmptd	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ 𝐶 ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
5		cncff	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
6	2 5	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7	6	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
8	7	reseq1d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ 𝐶 ) )
9		nfcv	⊢ Ⅎ 𝑦 𝐹
10		nfcv	⊢ Ⅎ 𝑦 𝑥
11	9 10	nffv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 )
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	1 12	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
14		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
15	11 13 14	cbvmpt	⊢ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) )
16	15	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
17	4 8 16	3eqtr4rd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ 𝐶 ) )
18		rescncf	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) )
19	3 2 18	sylc	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) )
20	17 19	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )