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

Theorem fco 5629
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 5487 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5487 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5582 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1157 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 453 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5165 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3342 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 653 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 454 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 530 . . . 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 420 . . 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 467 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5487 . 2  |-  ( ( F  o.  G ) : A --> C  <->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
1412, 13sylibr 205 1  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( F  o.  G ) : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    C_ wss 3306   ran crn 4908    o. ccom 4911    Fn wfn 5478   -->wf 5479
This theorem is referenced by:  fco2  5630  f1co  5677  foco  5692  mapen  7300  unxpwdom2  7585  mapfien  7682  wemapwe  7683  cofsmo  8180  cfcoflem  8183  isf34lem7  8290  isf34lem6  8291  canthp1lem2  8559  inar1  8681  addnqf  8856  mulnqf  8857  axdc4uzlem  11352  seqf1olem2  11394  wrdco  11831  lenco  11832  lo1o1  12357  o1co  12411  caucvgrlem2  12499  fsumcl2lem  12556  fsumadd  12563  fsummulc2  12598  fsumrelem  12617  supcvg  12666  algcvg  13098  cofucl  14116  setccatid  14270  yonedalem3b  14407  mhmco  14793  pwsco1mhm  14800  pwsco2mhm  14801  gsumwmhm  14821  gsumval3  15545  gsumzcl  15549  gsumzf1o  15550  gsumzaddlem  15557  gsumzmhm  15564  gsumzoppg  15570  gsumzinv  15571  gsumsub  15573  dprdf1o  15621  ablfaclem2  15675  psrass1lem  16473  psrnegcl  16491  coe1f2  16638  cnfldds  16744  cnco  17361  cnpco  17362  lmcnp  17399  cnmpt11  17726  cnmpt21  17734  qtopcn  17777  fmco  18024  flfcnp  18067  tsmsf1o  18205  tsmsmhm  18206  tsmssub  18209  imasdsf1olem  18434  comet  18574  nrmmetd  18653  isngp2  18675  isngp3  18676  tngngp2  18724  cnmet  18837  cnfldms  18841  cncfco  18968  cnfldcusp  19342  ovolfioo  19395  ovolficc  19396  ovolfsf  19399  ovollb  19406  ovolctb  19417  ovolicc2lem4  19447  ovolicc2  19449  volsup  19481  uniioovol  19502  uniioombllem3a  19507  uniioombllem3  19508  uniioombllem4  19509  uniioombllem5  19510  uniioombl  19512  mbfdm  19549  ismbfcn  19552  mbfres  19565  mbfimaopnlem  19576  cncombf  19579  limccnp  19809  dvcobr  19863  dvcof  19865  dvcjbr  19866  dvcj  19867  dvmptco  19889  dvlip2  19910  itgsubstlem  19963  coecj  20227  pserulm  20369  jensenlem2  20857  jensen  20858  amgmlem  20859  dchrinv  21076  vsfval  22145  imsdf  22212  lnocoi  22289  hocofi  23300  homco1  23335  homco2  23511  hmopco  23557  kbass2  23651  kbass5  23654  opsqrlem1  23674  opsqrlem6  23679  pjinvari  23725  mbfmco  24645  dstfrvclim1  24766  gamf  24858  subfacp1lem5  24901  circum  25142  fprodcl2lem  25307  fprodmul  25315  fproddiv  25316  fprodn0  25334  mblfinlem2  26280  mbfresfi  26289  ftc1anclem5  26322  ghomco  26596  rngohomco  26628  mapco2g  26807  diophrw  26855  dsmmbas2  27218  f1lindf  27307  lindfmm  27312  f1omvdconj  27404  pmtrfinv  27417  symgtrinv  27428  psgnunilem1  27431  hausgraph  27546  sblpnf  27554  stoweidlem31  27794  stoweidlem59  27822  tendococl  31667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-br 4238  df-opab 4292  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-fun 5485  df-fn 5486  df-f 5487
  Copyright terms: Public domain W3C validator