Theorem cncfmpt1f

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

	Ref	Expression
Hypotheses	cncfmpt1f.1	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$
	cncfmpt1f.2	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
Assertion	cncfmpt1f	$$⊢\phi \to \left(x\in X⟼F\left(A\right)\right):X\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		cncfmpt1f.1	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$
2		cncfmpt1f.2	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
3		cncff	$$⊢\left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ\to \left(x\in X⟼A\right):X⟶ℂ$$
4	2 3	syl	$$⊢\phi \to \left(x\in X⟼A\right):X⟶ℂ$$
5		eqid	$$⊢\left(x\in X⟼A\right)=\left(x\in X⟼A\right)$$
6	5	fmpt	$$⊢\forall x\in XA\in ℂ\leftrightarrow \left(x\in X⟼A\right):X⟶ℂ$$
7	4 6	sylibr	$$⊢\phi \to \forall x\in XA\in ℂ$$
8		eqidd	$$⊢\phi \to \left(x\in X⟼A\right)=\left(x\in X⟼A\right)$$
9		cncff	$$⊢F:ℂ\underset{cn}{⟶}ℂ\to F:ℂ⟶ℂ$$
10	1 9	syl	$$⊢\phi \to F:ℂ⟶ℂ$$
11	10	feqmptd	$$⊢\phi \to F=\left(y\in ℂ⟼F\left(y\right)\right)$$
12		fveq2	$$⊢y=A\to F\left(y\right)=F\left(A\right)$$
13	7 8 11 12	fmptcof	$$⊢\phi \to F\circ \left(x\in X⟼A\right)=\left(x\in X⟼F\left(A\right)\right)$$
14	2 1	cncfco	$$⊢\phi \to \left(F\circ \left(x\in X⟼A\right)\right):X\underset{cn}{⟶}ℂ$$
15	13 14	eqeltrrd	$$⊢\phi \to \left(x\in X⟼F\left(A\right)\right):X\underset{cn}{⟶}ℂ$$