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

Metamath Proof Explorer

Theorem cnmpt22f

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 ) )
cnmpt2t.b 
|- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
cnmpt22f.f 
|- ( ph -> F e. ( ( L tX M ) Cn N ) )
Assertion cnmpt22f 
|- ( ph -> ( x e. X , y e. Y |-> ( A F B ) ) e. ( ( J tX K ) Cn N ) )

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 cnmpt2t.b 
 |-  ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )
5 cnmpt22f.f 
 |-  ( ph -> F e. ( ( L tX M ) Cn N ) )
6 cntop2 
 |-  ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) -> L e. Top )
7 3 6 syl 
 |-  ( ph -> L e. Top )
8 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
9 7 8 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
10 cntop2 
 |-  ( ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) -> M e. Top )
11 4 10 syl 
 |-  ( ph -> M e. Top )
12 toptopon2 
 |-  ( M e. Top <-> M e. ( TopOn ` U. M ) )
13 11 12 sylib 
 |-  ( ph -> M e. ( TopOn ` U. M ) )
14 txtopon 
 |-  ( ( L e. ( TopOn ` U. L ) /\ M e. ( TopOn ` U. M ) ) -> ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) )
15 9 13 14 syl2anc 
 |-  ( ph -> ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) )
16 cntop2 
 |-  ( F e. ( ( L tX M ) Cn N ) -> N e. Top )
17 5 16 syl 
 |-  ( ph -> N e. Top )
18 toptopon2 
 |-  ( N e. Top <-> N e. ( TopOn ` U. N ) )
19 17 18 sylib 
 |-  ( ph -> N e. ( TopOn ` U. N ) )
20 cnf2 
 |-  ( ( ( L tX M ) e. ( TopOn ` ( U. L X. U. M ) ) /\ N e. ( TopOn ` U. N ) /\ F e. ( ( L tX M ) Cn N ) ) -> F : ( U. L X. U. M ) --> U. N )
21 15 19 5 20 syl3anc 
 |-  ( ph -> F : ( U. L X. U. M ) --> U. N )
22 21 ffnd 
 |-  ( ph -> F Fn ( U. L X. U. M ) )
23 fnov 
 |-  ( F Fn ( U. L X. U. M ) <-> F = ( z e. U. L , w e. U. M |-> ( z F w ) ) )
24 22 23 sylib 
 |-  ( ph -> F = ( z e. U. L , w e. U. M |-> ( z F w ) ) )
25 24 5 eqeltrrd 
 |-  ( ph -> ( z e. U. L , w e. U. M |-> ( z F w ) ) e. ( ( L tX M ) Cn N ) )
26 oveq12 
 |-  ( ( z = A /\ w = B ) -> ( z F w ) = ( A F B ) )
27 1 2 3 4 9 13 25 26 cnmpt22 
 |-  ( ph -> ( x e. X , y e. Y |-> ( A F B ) ) e. ( ( J tX K ) Cn N ) )