MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnco Structured version   Unicode version

Theorem cnco 19934
Description: The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnco  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( G  o.  F
)  e.  ( J  Cn  L ) )

Proof of Theorem cnco
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 cntop1 19908 . . 3  |-  ( F  e.  ( J  Cn  K )  ->  J  e.  Top )
2 cntop2 19909 . . 3  |-  ( G  e.  ( K  Cn  L )  ->  L  e.  Top )
31, 2anim12i 564 . 2  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( J  e.  Top  /\  L  e.  Top )
)
4 eqid 2454 . . . . 5  |-  U. K  =  U. K
5 eqid 2454 . . . . 5  |-  U. L  =  U. L
64, 5cnf 19914 . . . 4  |-  ( G  e.  ( K  Cn  L )  ->  G : U. K --> U. L
)
7 eqid 2454 . . . . 5  |-  U. J  =  U. J
87, 4cnf 19914 . . . 4  |-  ( F  e.  ( J  Cn  K )  ->  F : U. J --> U. K
)
9 fco 5723 . . . 4  |-  ( ( G : U. K --> U. L  /\  F : U. J --> U. K )  -> 
( G  o.  F
) : U. J --> U. L )
106, 8, 9syl2anr 476 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( G  o.  F
) : U. J --> U. L )
11 cnvco 5177 . . . . . . 7  |-  `' ( G  o.  F )  =  ( `' F  o.  `' G )
1211imaeq1i 5322 . . . . . 6  |-  ( `' ( G  o.  F
) " x )  =  ( ( `' F  o.  `' G
) " x )
13 imaco 5495 . . . . . 6  |-  ( ( `' F  o.  `' G ) " x
)  =  ( `' F " ( `' G " x ) )
1412, 13eqtri 2483 . . . . 5  |-  ( `' ( G  o.  F
) " x )  =  ( `' F " ( `' G "
x ) )
15 simpll 751 . . . . . 6  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  F  e.  ( J  Cn  K
) )
16 cnima 19933 . . . . . . 7  |-  ( ( G  e.  ( K  Cn  L )  /\  x  e.  L )  ->  ( `' G "
x )  e.  K
)
1716adantll 711 . . . . . 6  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' G " x )  e.  K )
18 cnima 19933 . . . . . 6  |-  ( ( F  e.  ( J  Cn  K )  /\  ( `' G " x )  e.  K )  -> 
( `' F "
( `' G "
x ) )  e.  J )
1915, 17, 18syl2anc 659 . . . . 5  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' F " ( `' G " x ) )  e.  J )
2014, 19syl5eqel 2546 . . . 4  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' ( G  o.  F ) " x
)  e.  J )
2120ralrimiva 2868 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  ->  A. x  e.  L  ( `' ( G  o.  F ) " x
)  e.  J )
2210, 21jca 530 . 2  |-  ( ( 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 ) )
237, 5iscn2 19906 . 2  |-  ( ( 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 ) ) )
243, 22, 23sylanbrc 662 1  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( G  o.  F
)  e.  ( J  Cn  L ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   A.wral 2804   U.cuni 4235   `'ccnv 4987   "cima 4991    o. ccom 4992   -->wf 5566  (class class class)co 6270   Topctop 19561    Cn ccn 19892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-map 7414  df-top 19566  df-topon 19569  df-cn 19895
This theorem is referenced by:  kgencn2  20224  txcn  20293  xkoco1cn  20324  xkoco2cn  20325  xkococnlem  20326  xkococn  20327  cnmpt11  20330  cnmpt21  20338  hmeoco  20439  qtophmeo  20484  htpyco1  21644  htpyco2  21645  phtpyco2  21656  reparphti  21663  reparpht  21664  phtpcco2  21665  copco  21684  pi1cof  21725  pi1coghm  21727  cnpcon  28939  txsconlem  28949  txscon  28950  cvmlift3lem2  29029  cvmlift3lem4  29031  cvmlift3lem5  29032  cvmlift3lem6  29033  hausgraph  31413
  Copyright terms: Public domain W3C validator