Metamath Proof Explorer

Theorem cnco

Description: The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnco 
|- ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) e. ( J Cn L ) )

Proof

Step Hyp Ref Expression
1 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
2 cntop2 
 |-  ( G e. ( K Cn L ) -> L e. Top )
3 1 2 anim12i 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( J e. Top /\ L e. Top ) )
4 eqid 
 |-  U. K = U. K
5 eqid 
 |-  U. L = U. L
6 4 5 cnf 
 |-  ( G e. ( K Cn L ) -> G : U. K --> U. L )
7 eqid 
 |-  U. J = U. J
8 7 4 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
9 fco 
 |-  ( ( G : U. K --> U. L /\ F : U. J --> U. K ) -> ( G o. F ) : U. J --> U. L )
10 6 8 9 syl2anr 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) : U. J --> U. L )
11 cnvco 
 |-  `' ( G o. F ) = ( `' F o. `' G )
12 11 imaeq1i 
 |-  ( `' ( G o. F ) " x ) = ( ( `' F o. `' G ) " x )
13 imaco 
 |-  ( ( `' F o. `' G ) " x ) = ( `' F " ( `' G " x ) )
14 12 13 eqtri 
 |-  ( `' ( G o. F ) " x ) = ( `' F " ( `' G " x ) )
15 simpll 
 |-  ( ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) /\ x e. L ) -> F e. ( J Cn K ) )
16 cnima 
 |-  ( ( G e. ( K Cn L ) /\ x e. L ) -> ( `' G " x ) e. K )
17 16 adantll 
 |-  ( ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) /\ x e. L ) -> ( `' G " x ) e. K )
18 cnima 
 |-  ( ( F e. ( J Cn K ) /\ ( `' G " x ) e. K ) -> ( `' F " ( `' G " x ) ) e. J )
19 15 17 18 syl2anc 
 |-  ( ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) /\ x e. L ) -> ( `' F " ( `' G " x ) ) e. J )
20 14 19 eqeltrid 
 |-  ( ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) /\ x e. L ) -> ( `' ( G o. F ) " x ) e. J )
21 20 ralrimiva 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> A. x e. L ( `' ( G o. F ) " x ) e. J )
22 10 21 jca 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( ( G o. F ) : U. J --> U. L /\ A. x e. L ( `' ( G o. F ) " x ) e. J ) )
23 7 5 iscn2 
 |-  ( ( G o. F ) e. ( J Cn L ) <-> ( ( J e. Top /\ L e. Top ) /\ ( ( G o. F ) : U. J --> U. L /\ A. x e. L ( `' ( G o. F ) " x ) e. J ) ) )
24 3 22 23 sylanbrc 
 |-  ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) e. ( J Cn L ) )