Theorem cnmpt12f

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 ) )
	cnmpt1t.b	|- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )
	cnmpt12f.f	|- ( ph -> F e. ( ( K tX L ) Cn M ) )
Assertion	cnmpt12f	|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( J Cn M ) )

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		cnmpt1t.b	|- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )
4		cnmpt12f.f	|- ( ph -> F e. ( ( K tX L ) Cn M ) )
5		df-ov	|- ( A F B ) = ( F ` <. A , B >. )
6	5	mpteq2i	|- ( x e. X |-> ( A F B ) ) = ( x e. X |-> ( F ` <. A , B >. ) )
7	1 2 3	cnmpt1t	|- ( ph -> ( x e. X |-> <. A , B >. ) e. ( J Cn ( K tX L ) ) )
8	1 7 4	cnmpt11f	|- ( ph -> ( x e. X |-> ( F ` <. A , B >. ) ) e. ( J Cn M ) )
9	6 8	eqeltrid	|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( J Cn M ) )