This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )