Theorem cnmpt21f

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	cnmpt21.j	|- ( ph -> J e. ( TopOn ` X ) )
	cnmpt21.k	|- ( ph -> K e. ( TopOn ` Y ) )
	cnmpt21.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
	cnmpt21f.f	|- ( ph -> F e. ( L Cn M ) )
Assertion	cnmpt21f	|- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	|- ( ph -> J e. ( TopOn ` X ) )
2		cnmpt21.k	|- ( ph -> K e. ( TopOn ` Y ) )
3		cnmpt21.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4		cnmpt21f.f	|- ( ph -> F e. ( L Cn M ) )
5		cntop1	|- ( F e. ( L Cn M ) -> L e. Top )
6	4 5	syl	|- ( ph -> L e. Top )
7		toptopon2	|- ( L e. Top <-> L e. ( TopOn ` U. L ) )
8	6 7	sylib	|- ( ph -> L e. ( TopOn ` U. L ) )
9		eqid	|- U. L = U. L
10		eqid	|- U. M = U. M
11	9 10	cnf	|- ( F e. ( L Cn M ) -> F : U. L --> U. M )
12	4 11	syl	|- ( ph -> F : U. L --> U. M )
13	12	feqmptd	|- ( ph -> F = ( z e. U. L |-> ( F ` z ) ) )
14	13 4	eqeltrrd	|- ( ph -> ( z e. U. L |-> ( F ` z ) ) e. ( L Cn M ) )
15		fveq2	|- ( z = A -> ( F ` z ) = ( F ` A ) )
16	1 2 3 8 14 15	cnmpt21	|- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )