Theorem cncfmpt1f

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

	Ref	Expression
Hypotheses	cncfmpt1f.1	|- ( ph -> F e. ( CC -cn-> CC ) )
	cncfmpt1f.2	|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
Assertion	cncfmpt1f	|- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( X -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmpt1f.1	|- ( ph -> F e. ( CC -cn-> CC ) )
2		cncfmpt1f.2	|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
3		cncff	|- ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> ( x e. X |-> A ) : X --> CC )
4	2 3	syl	|- ( ph -> ( x e. X |-> A ) : X --> CC )
5		eqid	|- ( x e. X |-> A ) = ( x e. X |-> A )
6	5	fmpt	|- ( A. x e. X A e. CC <-> ( x e. X |-> A ) : X --> CC )
7	4 6	sylibr	|- ( ph -> A. x e. X A e. CC )
8		eqidd	|- ( ph -> ( x e. X |-> A ) = ( x e. X |-> A ) )
9		cncff	|- ( F e. ( CC -cn-> CC ) -> F : CC --> CC )
10	1 9	syl	|- ( ph -> F : CC --> CC )
11	10	feqmptd	|- ( ph -> F = ( y e. CC |-> ( F ` y ) ) )
12		fveq2	|- ( y = A -> ( F ` y ) = ( F ` A ) )
13	7 8 11 12	fmptcof	|- ( ph -> ( F o. ( x e. X |-> A ) ) = ( x e. X |-> ( F ` A ) ) )
14	2 1	cncfco	|- ( ph -> ( F o. ( x e. X |-> A ) ) e. ( X -cn-> CC ) )
15	13 14	eqeltrrd	|- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( X -cn-> CC ) )