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

Theorem fco 5727
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 5578 . . 3  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
2 df-f 5578 . . 3  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
3 fnco 5675 . . . . . . 7  |-  ( ( F  Fn  B  /\  G  Fn  A  /\  ran  G  C_  B )  ->  ( F  o.  G
)  Fn  A )
433expib 1198 . . . . . 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 5249 . . . . . . 7  |-  ran  ( F  o.  G )  C_ 
ran  F
7 sstr 3494 . . . . . . 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 5578 . 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 3458   ran crn 4986    o. ccom 4989    Fn wfn 5569   -->wf 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-fun 5576  df-fn 5577  df-f 5578
This theorem is referenced by:  fco2  5728  f1co  5776  foco  5791  mapen  7679  fsuppco2  7860  mapfienlem1  7862  mapfienlem3  7864  mapfien  7865  unxpwdom2  8012  mapfienOLD  8136  wemapwe  8137  wemapweOLD  8138  cofsmo  8647  cfcoflem  8650  isf34lem7  8757  isf34lem6  8758  canthp1lem2  9029  inar1  9151  addnqf  9324  mulnqf  9325  axdc4uzlem  12066  seqf1olem2  12121  wrdco  12771  lenco  12772  lo1o1  13329  o1co  13383  caucvgrlem2  13471  fsumcl2lem  13527  fsumadd  13535  fsummulc2  13573  fsumrelem  13595  supcvg  13641  algcvg  14077  cofucl  15126  setccatid  15280  yonedalem3b  15417  mhmco  15862  pwsco1mhm  15870  pwsco2mhm  15871  gsumwmhm  15882  f1omvdconj  16340  pmtrfinv  16355  symgtrinv  16366  psgnunilem1  16387  gsumval3OLD  16777  gsumval3lem1  16778  gsumval3lem2  16779  gsumval3  16780  gsumzcl2  16784  gsumzf1o  16786  gsumzclOLD  16788  gsumzf1oOLD  16789  gsumzaddlem  16803  gsumzaddlemOLD  16805  gsumzmhm  16826  gsumzmhmOLD  16827  gsumzoppg  16836  gsumzoppgOLD  16837  gsumzinv  16838  gsumzinvOLD  16839  gsumsub  16843  gsumsubOLD  16844  dprdf1o  16947  ablfaclem2  17005  psrass1lem  17897  psrnegcl  17917  coe1f2  18116  cnfldds  18298  dsmmbas2  18635  f1lindf  18724  lindfmm  18729  cpmadumatpolylem1  19249  cnco  19633  cnpco  19634  lmcnp  19671  cnmpt11  20030  cnmpt21  20038  qtopcn  20081  fmco  20328  flfcnp  20371  tsmsf1o  20513  tsmsmhm  20514  tsmssub  20517  imasdsf1olem  20742  comet  20882  nrmmetd  20961  isngp2  20983  isngp3  20984  tngngp2  21032  cnmet  21145  cnfldms  21149  cncfco  21277  cnfldcusp  21663  ovolfioo  21745  ovolficc  21746  ovolfsf  21749  ovollb  21756  ovolctb  21767  ovolicc2lem4  21797  ovolicc2  21799  volsup  21832  uniioovol  21854  uniioombllem3a  21859  uniioombllem3  21860  uniioombllem4  21861  uniioombllem5  21862  uniioombl  21864  mbfdm  21901  ismbfcn  21904  mbfres  21917  mbfimaopnlem  21928  cncombf  21931  limccnp  22161  dvcobr  22215  dvcof  22217  dvcjbr  22218  dvcj  22219  dvmptco  22241  dvlip2  22262  itgsubstlem  22315  coecj  22540  pserulm  22682  jensenlem2  23182  jensen  23183  amgmlem  23184  dchrinv  23401  motcgrg  23796  vsfval  25393  imsdf  25460  lnocoi  25537  hocofi  26550  homco1  26585  homco2  26761  hmopco  26807  kbass2  26901  kbass5  26904  opsqrlem1  26924  opsqrlem6  26929  pjinvari  26975  fcobij  27413  fcobijfs  27414  mbfmco  28101  dstfrvclim1  28282  gamf  28451  subfacp1lem5  28494  mrsubco  28747  mclsppslem  28809  circum  28906  fprodcl2lem  29050  fprodmul  29058  fproddiv  29059  fprodn0  29077  mblfinlem2  30020  mbfresfi  30029  ftc1anclem5  30062  ghomco  30313  rngohomco  30345  mapco2g  30614  diophrw  30660  hausgraph  31141  sblpnf  31159  limccog  31530  mbfres2cn  31643  stoweidlem31  31698  stoweidlem59  31726  mgmhmco  32323  estrccatid  32476  tendococl  36200
  Copyright terms: Public domain W3C validator