Theorem cnmpt11f

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptid.j	|- ( ph -> J e. ( TopOn ` X ) )
	cnmpt11.a	|- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )
	cnmpt11f.f	|- ( ph -> F e. ( K Cn L ) )
Assertion	cnmpt11f	|- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( J Cn L ) )

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	|- ( ph -> J e. ( TopOn ` X ) )
2		cnmpt11.a	|- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )
3		cnmpt11f.f	|- ( ph -> F e. ( K Cn L ) )
4		cntop2	|- ( ( x e. X |-> A ) e. ( J Cn K ) -> K e. Top )
5	2 4	syl	|- ( ph -> K e. Top )
6		toptopon2	|- ( K e. Top <-> K e. ( TopOn ` U. K ) )
7	5 6	sylib	|- ( ph -> K e. ( TopOn ` U. K ) )
8		eqid	|- U. K = U. K
9		eqid	|- U. L = U. L
10	8 9	cnf	|- ( F e. ( K Cn L ) -> F : U. K --> U. L )
11	3 10	syl	|- ( ph -> F : U. K --> U. L )
12	11	feqmptd	|- ( ph -> F = ( y e. U. K |-> ( F ` y ) ) )
13	12 3	eqeltrrd	|- ( ph -> ( y e. U. K |-> ( F ` y ) ) e. ( K Cn L ) )
14		fveq2	|- ( y = A -> ( F ` y ) = ( F ` A ) )
15	1 2 7 13 14	cnmpt11	|- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( J Cn L ) )