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

Theorem cnco 18882
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 18856 . . 3  |-  ( F  e.  ( J  Cn  K )  ->  J  e.  Top )
2 cntop2 18857 . . 3  |-  ( G  e.  ( K  Cn  L )  ->  L  e.  Top )
31, 2anim12i 566 . 2  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( J  e.  Top  /\  L  e.  Top )
)
4 eqid 2443 . . . . 5  |-  U. K  =  U. K
5 eqid 2443 . . . . 5  |-  U. L  =  U. L
64, 5cnf 18862 . . . 4  |-  ( G  e.  ( K  Cn  L )  ->  G : U. K --> U. L
)
7 eqid 2443 . . . . 5  |-  U. J  =  U. J
87, 4cnf 18862 . . . 4  |-  ( F  e.  ( J  Cn  K )  ->  F : U. J --> U. K
)
9 fco 5580 . . . 4  |-  ( ( G : U. K --> U. L  /\  F : U. J --> U. K )  -> 
( G  o.  F
) : U. J --> U. L )
106, 8, 9syl2anr 478 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  -> 
( G  o.  F
) : U. J --> U. L )
11 cnvco 5037 . . . . . . 7  |-  `' ( G  o.  F )  =  ( `' F  o.  `' G )
1211imaeq1i 5178 . . . . . 6  |-  ( `' ( G  o.  F
) " x )  =  ( ( `' F  o.  `' G
) " x )
13 imaco 5355 . . . . . 6  |-  ( ( `' F  o.  `' G ) " x
)  =  ( `' F " ( `' G " x ) )
1412, 13eqtri 2463 . . . . 5  |-  ( `' ( G  o.  F
) " x )  =  ( `' F " ( `' G "
x ) )
15 simpll 753 . . . . . 6  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  F  e.  ( J  Cn  K
) )
16 cnima 18881 . . . . . . 7  |-  ( ( G  e.  ( K  Cn  L )  /\  x  e.  L )  ->  ( `' G "
x )  e.  K
)
1716adantll 713 . . . . . 6  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' G " x )  e.  K )
18 cnima 18881 . . . . . 6  |-  ( ( F  e.  ( J  Cn  K )  /\  ( `' G " x )  e.  K )  -> 
( `' F "
( `' G "
x ) )  e.  J )
1915, 17, 18syl2anc 661 . . . . 5  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' F " ( `' G " x ) )  e.  J )
2014, 19syl5eqel 2527 . . . 4  |-  ( ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  /\  x  e.  L )  ->  ( `' ( G  o.  F ) " x
)  e.  J )
2120ralrimiva 2811 . . 3  |-  ( ( F  e.  ( J  Cn  K )  /\  G  e.  ( K  Cn  L ) )  ->  A. x  e.  L  ( `' ( G  o.  F ) " x
)  e.  J )
2210, 21jca 532 . 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 18854 . 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 664 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 369    e. wcel 1756   A.wral 2727   U.cuni 4103   `'ccnv 4851   "cima 4855    o. ccom 4856   -->wf 5426  (class class class)co 6103   Topctop 18510    Cn ccn 18840
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-fv 5438  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-map 7228  df-top 18515  df-topon 18518  df-cn 18843
This theorem is referenced by:  kgencn2  19142  txcn  19211  xkoco1cn  19242  xkoco2cn  19243  xkococnlem  19244  xkococn  19245  cnmpt11  19248  cnmpt21  19256  hmeoco  19357  qtophmeo  19402  htpyco1  20562  htpyco2  20563  phtpyco2  20574  reparphti  20581  reparpht  20582  phtpcco2  20583  copco  20602  pi1cof  20643  pi1coghm  20645  cnpcon  27131  txsconlem  27141  txscon  27142  cvmlift3lem2  27221  cvmlift3lem4  27223  cvmlift3lem5  27224  cvmlift3lem6  27225  hausgraph  29592
  Copyright terms: Public domain W3C validator