Theorem cncfmpt1f

Description: Composition of continuous functions. -cn-> analogue of cnmpt11f . (Contributed by Mario Carneiro, 3-Sep-2014)

	Ref	Expression
Hypotheses	cncfmpt1f.1	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
	cncfmpt1f.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion	cncfmpt1f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmpt1f.1	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )
2		cncfmpt1f.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
3		cncff	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
4	2 3	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
5		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
6	5	fmpt	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ℂ ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
7	4 6	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ℂ )
8		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
9		cncff	⊢ ( 𝐹 ∈ ( ℂ –cn→ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
10	1 9	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
11	10	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℂ ↦ ( 𝐹 ‘ 𝑦 ) ) )
12		fveq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
13	7 8 11 12	fmptcof	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) )
14	2 1	cncfco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
15	13 14	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ ( 𝑋 –cn→ ℂ ) )