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

Theorem fco 5559
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 5417 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5417 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5512 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1156 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 452 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5095 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3316 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 652 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 453 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 529 . . . 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 419 . . 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 466 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5417 . 2  |-  ( ( F  o.  G ) : A --> C  <->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
1412, 13sylibr 204 1  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3280   ran crn 4838    o. ccom 4841    Fn wfn 5408   -->wf 5409
This theorem is referenced by:  fco2  5560  f1co  5607  foco  5622  mapen  7230  unxpwdom2  7512  mapfien  7609  wemapwe  7610  cofsmo  8105  cfcoflem  8108  isf34lem7  8215  isf34lem6  8216  canthp1lem2  8484  inar1  8606  addnqf  8781  mulnqf  8782  axdc4uzlem  11276  seqf1olem2  11318  wrdco  11755  lenco  11756  lo1o1  12281  o1co  12335  caucvgrlem2  12423  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumrelem  12541  supcvg  12590  algcvg  13022  cofucl  14040  setccatid  14194  yonedalem3b  14331  mhmco  14717  pwsco1mhm  14724  pwsco2mhm  14725  gsumwmhm  14745  gsumval3  15469  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumzmhm  15488  gsumzoppg  15494  gsumzinv  15495  gsumsub  15497  dprdf1o  15545  ablfaclem2  15599  psrass1lem  16397  psrnegcl  16415  coe1f2  16562  cnfldds  16668  cnco  17284  cnpco  17285  lmcnp  17322  cnmpt11  17648  cnmpt21  17656  qtopcn  17699  fmco  17946  flfcnp  17989  tsmsf1o  18127  tsmsmhm  18128  tsmssub  18131  imasdsf1olem  18356  comet  18496  nrmmetd  18575  isngp2  18597  isngp3  18598  tngngp2  18646  cnmet  18759  cnfldms  18763  cncfco  18890  cnfldcusp  19264  ovolfioo  19317  ovolficc  19318  ovolfsf  19321  ovollb  19328  ovolctb  19339  ovolicc2lem4  19369  ovolicc2  19371  volsup  19403  uniioovol  19424  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  mbfdm  19473  ismbfcn  19476  mbfres  19489  mbfimaopnlem  19500  cncombf  19503  limccnp  19731  dvcobr  19785  dvcof  19787  dvcjbr  19788  dvcj  19789  dvmptco  19811  dvlip2  19832  itgsubstlem  19885  coecj  20149  pserulm  20291  jensenlem2  20779  jensen  20780  amgmlem  20781  dchrinv  20998  vsfval  22067  imsdf  22134  lnocoi  22211  hocofi  23222  homco1  23257  homco2  23433  hmopco  23479  kbass2  23573  kbass5  23576  opsqrlem1  23596  opsqrlem6  23601  pjinvari  23647  mbfmco  24567  dstfrvclim1  24688  gamf  24780  subfacp1lem5  24823  circum  25064  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodn0  25256  mblfinlem  26143  mbfresfi  26152  ghomco  26448  rngohomco  26480  mapco2g  26659  diophrw  26707  dsmmbas2  27071  f1lindf  27160  lindfmm  27165  f1omvdconj  27257  pmtrfinv  27270  symgtrinv  27281  psgnunilem1  27284  hausgraph  27399  sblpnf  27407  stoweidlem31  27647  stoweidlem59  27675  tendococl  31254
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5415  df-fn 5416  df-f 5417
  Copyright terms: Public domain W3C validator