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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
	cncfmptssg.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
	cncfmptssg.4	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	cncfmptssg.5	⊢ ( 𝜑 → 𝐷 ⊆ 𝐵 )
	cncfmptssg.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐸 ∈ 𝐷 )
Assertion	cncfmptssg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmptssg.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
2		cncfmptssg.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
3		cncfmptssg.4	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4		cncfmptssg.5	⊢ ( 𝜑 → 𝐷 ⊆ 𝐵 )
5		cncfmptssg.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐸 ∈ 𝐷 )
6	5	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 )
7		cncfrss2	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐵 ⊆ ℂ )
8	2 7	syl	⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
9	4 8	sstrd	⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
10	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
11	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐸 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) = 𝐸 )
12	10 5 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐸 )
13	12	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) )
14		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
15	1 14	nfcxfr	⊢ Ⅎ 𝑥 𝐹
16	15 2 3	cncfmptss	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )
17	13 16	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐵 ) )
18		cncffvrn	⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 ) )
19	9 17 18	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 ) )
20	6 19	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) )