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

Metamath Proof Explorer

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