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

Theorem fco 5580
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 5434 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5434 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5531 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1190 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 465 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5112 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3376 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 670 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 466 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 544 . . . 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 429 . . 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 479 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5434 . 2  |-  ( ( F  o.  G ) : A --> C  <->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
1412, 13sylibr 212 1  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3340   ran crn 4853    o. ccom 4856    Fn wfn 5425   -->wf 5426
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-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543
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-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5432  df-fn 5433  df-f 5434
This theorem is referenced by:  fco2  5581  f1co  5627  foco  5642  mapen  7487  fsuppco2  7664  mapfienlem1  7666  mapfienlem3  7668  mapfien  7669  unxpwdom2  7815  mapfienOLD  7939  wemapwe  7940  wemapweOLD  7941  cofsmo  8450  cfcoflem  8453  isf34lem7  8560  isf34lem6  8561  canthp1lem2  8832  inar1  8954  addnqf  9129  mulnqf  9130  axdc4uzlem  11816  seqf1olem2  11858  wrdco  12471  lenco  12472  lo1o1  13022  o1co  13076  caucvgrlem2  13164  fsumcl2lem  13220  fsumadd  13227  fsummulc2  13263  fsumrelem  13282  supcvg  13330  algcvg  13763  cofucl  14810  setccatid  14964  yonedalem3b  15101  mhmco  15502  pwsco1mhm  15510  pwsco2mhm  15511  gsumwmhm  15535  f1omvdconj  15964  pmtrfinv  15979  symgtrinv  15990  psgnunilem1  16011  gsumval3OLD  16394  gsumval3lem1  16395  gsumval3lem2  16396  gsumval3  16397  gsumzcl2  16401  gsumzf1o  16403  gsumzclOLD  16405  gsumzf1oOLD  16406  gsumzaddlem  16420  gsumzaddlemOLD  16422  gsumzmhm  16442  gsumzmhmOLD  16443  gsumzoppg  16452  gsumzoppgOLD  16453  gsumzinv  16454  gsumzinvOLD  16455  gsumsub  16459  gsumsubOLD  16460  dprdf1o  16541  ablfaclem2  16599  psrass1lem  17459  psrnegcl  17479  coe1f2  17677  cnfldds  17840  dsmmbas2  18174  f1lindf  18263  lindfmm  18268  cnco  18882  cnpco  18883  lmcnp  18920  cnmpt11  19248  cnmpt21  19256  qtopcn  19299  fmco  19546  flfcnp  19589  tsmsf1o  19731  tsmsmhm  19732  tsmssub  19735  imasdsf1olem  19960  comet  20100  nrmmetd  20179  isngp2  20201  isngp3  20202  tngngp2  20250  cnmet  20363  cnfldms  20367  cncfco  20495  cnfldcusp  20881  ovolfioo  20963  ovolficc  20964  ovolfsf  20967  ovollb  20974  ovolctb  20985  ovolicc2lem4  21015  ovolicc2  21017  volsup  21049  uniioovol  21071  uniioombllem3a  21076  uniioombllem3  21077  uniioombllem4  21078  uniioombllem5  21079  uniioombl  21081  mbfdm  21118  ismbfcn  21121  mbfres  21134  mbfimaopnlem  21145  cncombf  21148  limccnp  21378  dvcobr  21432  dvcof  21434  dvcjbr  21435  dvcj  21436  dvmptco  21458  dvlip2  21479  itgsubstlem  21532  coecj  21757  pserulm  21899  jensenlem2  22393  jensen  22394  amgmlem  22395  dchrinv  22612  vsfval  24025  imsdf  24092  lnocoi  24169  hocofi  25182  homco1  25217  homco2  25393  hmopco  25439  kbass2  25533  kbass5  25536  opsqrlem1  25556  opsqrlem6  25561  pjinvari  25607  fcobij  26037  fcobijfs  26038  mbfmco  26691  dstfrvclim1  26872  gamf  27041  subfacp1lem5  27084  circum  27331  fprodcl2lem  27475  fprodmul  27483  fproddiv  27484  fprodn0  27502  mblfinlem2  28441  mbfresfi  28450  ftc1anclem5  28483  ghomco  28760  rngohomco  28792  mapco2g  29062  diophrw  29109  hausgraph  29592  sblpnf  29608  stoweidlem31  29838  stoweidlem59  29866  tendococl  34428
  Copyright terms: Public domain W3C validator