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

Theorem fco 5723
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 5574 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5574 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5671 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1197 . . . . . 6  |-  ( F  Fn  B  ->  (
( G  Fn  A  /\  ran  G  C_  B
)  ->  ( F  o.  G )  Fn  A
) )
54adantr 463 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ( ( G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G )  Fn  A ) )
6 rncoss 5252 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3497 . . . . . . 7  |-  ( ( ran  ( F  o.  G )  C_  ran  F  /\  ran  F  C_  C )  ->  ran  ( F  o.  G
)  C_  C )
86, 7mpan 668 . . . . . 6  |-  ( ran 
F  C_  C  ->  ran  ( F  o.  G
)  C_  C )
98adantl 464 . . . . 5  |-  ( ( F  Fn  B  /\  ran  F  C_  C )  ->  ran  ( F  o.  G )  C_  C
)
105, 9jctird 542 . . . 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 427 . . 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 477 . 2  |-  ( ( F : B --> C  /\  G : A --> B )  ->  ( ( F  o.  G )  Fn  A  /\  ran  ( F  o.  G )  C_  C ) )
13 df-f 5574 . 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 367    C_ wss 3461   ran crn 4989    o. ccom 4992    Fn wfn 5565   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-fun 5572  df-fn 5573  df-f 5574
This theorem is referenced by:  fco2  5724  f1co  5772  foco  5787  mapen  7674  fsuppco2  7854  mapfienlem1  7856  mapfienlem3  7858  mapfien  7859  unxpwdom2  8006  mapfienOLD  8129  wemapwe  8130  wemapweOLD  8131  cofsmo  8640  cfcoflem  8643  isf34lem7  8750  isf34lem6  8751  canthp1lem2  9020  inar1  9142  addnqf  9315  mulnqf  9316  axdc4uzlem  12074  seqf1olem2  12129  wrdco  12788  lenco  12789  lo1o1  13437  o1co  13491  caucvgrlem2  13579  fsumcl2lem  13635  fsumadd  13643  fsummulc2  13681  fsumrelem  13703  supcvg  13749  fprodcl2lem  13839  fprodmul  13847  fproddiv  13848  fprodn0  13865  algcvg  14289  cofucl  15376  setccatid  15562  estrccatid  15600  funcestrcsetclem9  15616  funcsetcestrclem9  15631  yonedalem3b  15747  mhmco  16192  pwsco1mhm  16200  pwsco2mhm  16201  gsumwmhm  16212  f1omvdconj  16670  pmtrfinv  16685  symgtrinv  16696  psgnunilem1  16717  gsumval3OLD  17107  gsumval3lem1  17108  gsumval3lem2  17109  gsumval3  17110  gsumzcl2  17114  gsumzf1o  17116  gsumzclOLD  17118  gsumzf1oOLD  17119  gsumzaddlem  17133  gsumzaddlemOLD  17135  gsumzmhm  17155  gsumzmhmOLD  17156  gsumzoppg  17165  gsumzoppgOLD  17166  gsumzinv  17167  gsumzinvOLD  17168  gsumsub  17171  dprdf1o  17274  ablfaclem2  17332  psrass1lem  18224  psrnegcl  18244  coe1f2  18443  cnfldds  18625  dsmmbas2  18941  f1lindf  19024  lindfmm  19029  cpmadumatpolylem1  19549  cnco  19934  cnpco  19935  lmcnp  19972  cnmpt11  20330  cnmpt21  20338  qtopcn  20381  fmco  20628  flfcnp  20671  tsmsf1o  20813  tsmsmhm  20814  tsmssub  20817  imasdsf1olem  21042  comet  21182  nrmmetd  21261  isngp2  21283  isngp3  21284  tngngp2  21332  cnmet  21445  cnfldms  21449  cncfco  21577  cnfldcusp  21963  ovolfioo  22045  ovolficc  22046  ovolfsf  22049  ovollb  22056  ovolctb  22067  ovolicc2lem4  22097  ovolicc2  22099  volsup  22132  uniioovol  22154  uniioombllem3a  22159  uniioombllem3  22160  uniioombllem4  22161  uniioombllem5  22162  uniioombl  22164  mbfdm  22201  ismbfcn  22204  mbfres  22217  mbfimaopnlem  22228  cncombf  22231  limccnp  22461  dvcobr  22515  dvcof  22517  dvcjbr  22518  dvcj  22519  dvmptco  22541  dvlip2  22562  itgsubstlem  22615  coecj  22841  pserulm  22983  jensenlem2  23515  jensen  23516  amgmlem  23517  dchrinv  23734  motcgrg  24132  vsfval  25726  imsdf  25793  lnocoi  25870  hocofi  26883  homco1  26918  homco2  27094  hmopco  27140  kbass2  27234  kbass5  27237  opsqrlem1  27257  opsqrlem6  27262  pjinvari  27308  fcobij  27779  fcobijfs  27780  mbfmco  28472  dstfrvclim1  28680  gamf  28849  subfacp1lem5  28892  mrsubco  29145  mclsppslem  29207  circum  29304  mblfinlem2  30292  mbfresfi  30301  ftc1anclem5  30334  ghomco  30585  rngohomco  30617  mapco2g  30886  diophrw  30931  hausgraph  31413  sblpnf  31431  limccog  31865  mbfres2cn  31996  stoweidlem31  32052  stoweidlem59  32080  mgmhmco  32861  tendococl  36895
  Copyright terms: Public domain W3C validator