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

Theorem fco 5398
Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fco  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )

Proof of Theorem fco
StepHypRef Expression
1 df-f 5259 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5259 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5352 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1154 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 451 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 4945 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3187 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 651 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 452 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 528 . . . 4  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  (
( F  o.  G
)  Fn  A  /\  ran  ( F  o.  G
)  C_  C )
) )
1110imp 418 . . 3  |-  ( ( ( F  Fn  B  /\  ran  F  C_  C
)  /\  ( G  Fn  A  /\  ran  G  C_  B ) )  -> 
( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C
) )
121, 2, 11syl2anb 465 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5259 . 2  |-  ( ( F  o.  G ) : A --> C  <->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
1412, 13sylibr 203 1  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152   ran crn 4690    o. ccom 4693    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fco2  5399  f1co  5446  foco  5461  mapen  7025  unxpwdom2  7302  mapfien  7399  wemapwe  7400  cofsmo  7895  cfcoflem  7898  isf34lem7  8005  isf34lem6  8006  canthp1lem2  8275  inar1  8397  addnqf  8572  mulnqf  8573  axdc4uzlem  11044  seqf1olem2  11086  wrdco  11486  lenco  11487  lo1o1  12006  o1co  12060  caucvgrlem2  12147  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumrelem  12265  supcvg  12314  algcvg  12746  cofucl  13762  setccatid  13916  yonedalem3b  14053  mhmco  14439  pwsco1mhm  14446  pwsco2mhm  14447  gsumwmhm  14467  gsumval3  15191  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumzmhm  15210  gsumzoppg  15216  gsumzinv  15217  gsumsub  15219  dprdf1o  15267  ablfaclem2  15321  psrass1lem  16123  psrnegcl  16141  coe1f2  16290  cnfldds  16389  cnco  16995  cnpco  16996  lmcnp  17032  cnmpt11  17357  cnmpt21  17365  qtopcn  17405  fmco  17656  flfcnp  17699  tsmsf1o  17827  tsmsmhm  17828  tsmssub  17831  imasdsf1olem  17937  comet  18059  nrmmetd  18097  isngp2  18119  isngp3  18120  tngngp2  18168  cnmet  18281  cnfldms  18285  cncfco  18411  ovolfioo  18827  ovolficc  18828  ovolfsf  18831  ovollb  18838  ovolctb  18849  ovolicc2lem4  18879  ovolicc2  18881  volsup  18913  uniioovol  18934  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  mbfdm  18983  ismbfcn  18986  mbfres  18999  mbfimaopnlem  19010  cncombf  19013  limccnp  19241  dvcobr  19295  dvcof  19297  dvcjbr  19298  dvcj  19299  dvmptco  19321  dvlip2  19342  itgsubstlem  19395  coecj  19659  pserulm  19798  jensenlem2  20282  jensen  20283  amgmlem  20284  dchrinv  20500  vsfval  21191  imsdf  21258  lnocoi  21335  hocofi  22346  homco1  22381  homco2  22557  hmopco  22603  kbass2  22697  kbass5  22700  opsqrlem1  22720  opsqrlem6  22725  pjinvari  22771  subfacp1lem5  23126  circum  23418  surjsec2  24532  mapmapmap  24560  injsurinj  24561  cmptdst  24980  cmptdst2  24983  rocatval  25371  ghomco  25985  rngohomco  26017  mapco2g  26202  diophrw  26250  dsmmbas2  26615  f1lindf  26704  lindfmm  26709  f1omvdconj  26801  pmtrfinv  26814  symgtrinv  26825  psgnunilem1  26828  hausgraph  26943  sblpnf  26951  stoweidlem31  27192  stoweidlem59  27220  tendococl  30334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-fun 5257  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator