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

Theorem fco 5565
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 5419 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5419 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5516 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1185 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 462 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5096 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3361 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 665 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 463 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 541 . . . 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 476 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5419 . 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 3325   ran crn 4837    o. ccom 4840    Fn wfn 5410   -->wf 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-fun 5417  df-fn 5418  df-f 5419
This theorem is referenced by:  fco2  5566  f1co  5612  foco  5627  mapen  7471  fsuppco2  7648  mapfienlem1  7650  mapfienlem3  7652  mapfien  7653  unxpwdom2  7799  mapfienOLD  7923  wemapwe  7924  wemapweOLD  7925  cofsmo  8434  cfcoflem  8437  isf34lem7  8544  isf34lem6  8545  canthp1lem2  8816  inar1  8938  addnqf  9113  mulnqf  9114  axdc4uzlem  11800  seqf1olem2  11842  wrdco  12455  lenco  12456  lo1o1  13006  o1co  13060  caucvgrlem2  13148  fsumcl2lem  13204  fsumadd  13211  fsummulc2  13247  fsumrelem  13266  supcvg  13314  algcvg  13747  cofucl  14794  setccatid  14948  yonedalem3b  15085  mhmco  15485  pwsco1mhm  15493  pwsco2mhm  15494  gsumwmhm  15516  f1omvdconj  15945  pmtrfinv  15960  symgtrinv  15971  psgnunilem1  15992  gsumval3OLD  16375  gsumval3lem1  16376  gsumval3lem2  16377  gsumval3  16378  gsumzcl2  16382  gsumzf1o  16384  gsumzclOLD  16386  gsumzf1oOLD  16387  gsumzaddlem  16401  gsumzaddlemOLD  16403  gsumzmhm  16422  gsumzmhmOLD  16423  gsumzoppg  16432  gsumzoppgOLD  16433  gsumzinv  16434  gsumzinvOLD  16435  gsumsub  16439  gsumsubOLD  16440  dprdf1o  16519  ablfaclem2  16577  psrass1lem  17425  psrnegcl  17445  coe1f2  17641  cnfldds  17787  dsmmbas2  18121  f1lindf  18210  lindfmm  18215  cnco  18829  cnpco  18830  lmcnp  18867  cnmpt11  19195  cnmpt21  19203  qtopcn  19246  fmco  19493  flfcnp  19536  tsmsf1o  19678  tsmsmhm  19679  tsmssub  19682  imasdsf1olem  19907  comet  20047  nrmmetd  20126  isngp2  20148  isngp3  20149  tngngp2  20197  cnmet  20310  cnfldms  20314  cncfco  20442  cnfldcusp  20828  ovolfioo  20910  ovolficc  20911  ovolfsf  20914  ovollb  20921  ovolctb  20932  ovolicc2lem4  20962  ovolicc2  20964  volsup  20996  uniioovol  21018  uniioombllem3a  21023  uniioombllem3  21024  uniioombllem4  21025  uniioombllem5  21026  uniioombl  21028  mbfdm  21065  ismbfcn  21068  mbfres  21081  mbfimaopnlem  21092  cncombf  21095  limccnp  21325  dvcobr  21379  dvcof  21381  dvcjbr  21382  dvcj  21383  dvmptco  21405  dvlip2  21426  itgsubstlem  21479  coecj  21704  pserulm  21846  jensenlem2  22340  jensen  22341  amgmlem  22342  dchrinv  22559  vsfval  23948  imsdf  24015  lnocoi  24092  hocofi  25105  homco1  25140  homco2  25316  hmopco  25362  kbass2  25456  kbass5  25459  opsqrlem1  25479  opsqrlem6  25484  pjinvari  25530  fcobij  25960  fcobijfs  25961  mbfmco  26615  dstfrvclim1  26790  gamf  26959  subfacp1lem5  27002  circum  27248  fprodcl2lem  27392  fprodmul  27400  fproddiv  27401  fprodn0  27419  mblfinlem2  28354  mbfresfi  28363  ftc1anclem5  28396  ghomco  28673  rngohomco  28705  mapco2g  28975  diophrw  29022  hausgraph  29505  sblpnf  29521  stoweidlem31  29751  stoweidlem59  29779  tendococl  34138
  Copyright terms: Public domain W3C validator