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

Metamath Proof Explorer

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