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

Theorem fco 5761
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 5604 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5604 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5705 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1218 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 471 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5113 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3451 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 681 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 472 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 551 . . . 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 435 . . 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 486 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5604 . 2  |-  ( ( F  o.  G ) : A --> C  <->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
1412, 13sylibr 217 1  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    C_ wss 3415   ran crn 4853    o. ccom 4856    Fn wfn 5595   -->wf 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5602  df-fn 5603  df-f 5604
This theorem is referenced by:  fco2  5762  f1co  5810  foco  5825  mapen  7761  fsuppco2  7941  mapfienlem1  7943  mapfienlem3  7945  mapfien  7946  unxpwdom2  8128  wemapwe  8227  cofsmo  8724  cfcoflem  8727  isf34lem7  8834  isf34lem6  8835  canthp1lem2  9103  inar1  9225  addnqf  9398  mulnqf  9399  axdc4uzlem  12226  seqf1olem2  12284  wrdco  12964  lenco  12965  lo1o1  13644  o1co  13698  caucvgrlem2  13788  fsumcl2lem  13845  fsumadd  13853  fsummulc2  13893  fsumrelem  13915  supcvg  13962  fprodcl2lem  14052  fprodmul  14062  fproddiv  14063  fprodn0  14081  algcvg  14583  cofucl  15841  setccatid  16027  estrccatid  16065  funcestrcsetclem9  16081  funcsetcestrclem9  16096  yonedalem3b  16212  mhmco  16657  pwsco1mhm  16665  pwsco2mhm  16666  gsumwmhm  16677  f1omvdconj  17135  pmtrfinv  17150  symgtrinv  17161  psgnunilem1  17182  gsumval3lem1  17587  gsumval3lem2  17588  gsumval3  17589  gsumzcl2  17592  gsumzf1o  17594  gsumzaddlem  17602  gsumzmhm  17618  gsumzoppg  17625  gsumzinv  17626  gsumsub  17629  dprdf1o  17713  ablfaclem2  17767  psrass1lem  18649  psrnegcl  18668  coe1f2  18850  cnfldds  19028  dsmmbas2  19348  f1lindf  19428  lindfmm  19433  cpmadumatpolylem1  19953  cnco  20330  cnpco  20331  lmcnp  20368  cnmpt11  20726  cnmpt21  20734  qtopcn  20777  fmco  21024  flfcnp  21067  tsmsf1o  21207  tsmsmhm  21208  tsmssub  21211  imasdsf1olem  21436  comet  21576  nrmmetd  21637  isngp2  21659  isngp3  21660  tngngp2  21708  cnmet  21840  cnfldms  21844  cncfco  21987  cnfldcusp  22372  ovolfioo  22468  ovolficc  22469  ovolfsf  22472  ovollb  22480  ovolctb  22491  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  ovolicc2  22524  volsup  22557  uniioovol  22584  uniioombllem3a  22590  uniioombllem3  22591  uniioombllem4  22592  uniioombllem5  22593  uniioombl  22595  mbfdm  22632  ismbfcn  22635  mbfres  22648  mbfimaopnlem  22659  cncombf  22662  limccnp  22894  dvcobr  22948  dvcof  22950  dvcjbr  22951  dvcj  22952  dvmptco  22974  dvlip2  22995  itgsubstlem  23048  coecj  23280  pserulm  23425  jensenlem2  23961  jensen  23962  amgmlem  23963  gamf  24016  dchrinv  24237  motcgrg  24637  vsfval  26302  imsdf  26369  lnocoi  26446  hocofi  27467  homco1  27502  homco2  27678  hmopco  27724  kbass2  27818  kbass5  27821  opsqrlem1  27841  opsqrlem6  27846  pjinvari  27892  fcobij  28358  fcobijfs  28359  mbfmco  29134  dstfrvclim1  29358  subfacp1lem5  29955  mrsubco  30207  mclsppslem  30269  circum  30366  mblfinlem2  32022  mbfresfi  32031  ftc1anclem5  32065  ghomco  32225  rngohomco  32257  tendococl  34383  mapco2g  35600  diophrw  35645  hausgraph  36133  sblpnf  36701  limccog  37737  mbfres2cn  37872  stoweidlem31  37929  stoweidlem59  37957  sge0resrnlem  38282  hoicvr  38407  mgmhmco  40073
  Copyright terms: Public domain W3C validator