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

Theorem fco 6525
Description: Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fco ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)

Proof of Theorem fco
StepHypRef Expression
1 df-f 6353 . . 3 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
2 df-f 6353 . . 3 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
3 fnco 6459 . . . . . . 7 ((𝐹 Fn 𝐵𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴)
433expib 1118 . . . . . 6 (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
54adantr 483 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
6 rncoss 5837 . . . . . . 7 ran (𝐹𝐺) ⊆ ran 𝐹
7 sstr 3974 . . . . . . 7 ((ran (𝐹𝐺) ⊆ ran 𝐹 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
86, 7mpan 688 . . . . . 6 (ran 𝐹𝐶 → ran (𝐹𝐺) ⊆ 𝐶)
98adantl 484 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
105, 9jctird 529 . . . 4 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶)))
1110imp 409 . . 3 (((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
121, 2, 11syl2anb 599 . 2 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
13 df-f 6353 . 2 ((𝐹𝐺):𝐴𝐶 ↔ ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
1412, 13sylibr 236 1 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wss 3935  ran crn 5550  ccom 5553   Fn wfn 6344  wf 6345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-fun 6351  df-fn 6352  df-f 6353
This theorem is referenced by:  fcod  6526  fco2  6527  f1co  6579  foco  6596  mapen  8675  fsuppco2  8860  mapfienlem1  8862  mapfienlem3  8864  mapfien  8865  unxpwdom2  9046  wemapwe  9154  cofsmo  9685  cfcoflem  9688  isf34lem7  9795  isf34lem6  9796  canthp1lem2  10069  inar1  10191  addnqf  10364  mulnqf  10365  axdc4uzlem  13345  seqf1olem2  13404  wrdco  14187  lenco  14188  lo1o1  14883  o1co  14937  caucvgrlem2  15025  fsumcl2lem  15082  fsumadd  15090  fsummulc2  15133  fsumrelem  15156  supcvg  15205  fprodcl2lem  15298  fprodmul  15308  fproddiv  15309  fprodn0  15327  algcvg  15914  cofucl  17152  setccatid  17338  estrccatid  17376  funcestrcsetclem9  17392  funcsetcestrclem9  17407  yonedalem3b  17523  mhmco  17982  pwsco1mhm  17990  pwsco2mhm  17991  gsumwmhm  18004  efmndcl  18041  f1omvdconj  18568  pmtrfinv  18583  symgtrinv  18594  psgnunilem1  18615  gsumval3lem1  19019  gsumval3lem2  19020  gsumval3  19021  gsumzcl2  19024  gsumzf1o  19026  gsumzaddlem  19035  gsumzmhm  19051  gsumzoppg  19058  gsumzinv  19059  gsumsub  19062  dprdf1o  19148  ablfaclem2  19202  psrass1lem  20151  psrnegcl  20170  coe1f2  20371  cnfldds  20549  dsmmbas2  20875  f1lindf  20960  lindfmm  20965  cpmadumatpolylem1  21483  cnco  21868  cnpco  21869  lmcnp  21906  cnmpt11  22265  cnmpt21  22273  qtopcn  22316  fmco  22563  flfcnp  22606  tsmsf1o  22747  tsmsmhm  22748  tsmssub  22751  imasdsf1olem  22977  comet  23117  nrmmetd  23178  isngp2  23200  isngp3  23201  tngngp2  23255  cnmet  23374  cnfldms  23378  cncfco  23509  cnfldcusp  23954  ovolfioo  24062  ovolficc  24063  ovolfsf  24066  ovollb  24074  ovolctb  24085  ovolicc2lem4  24115  ovolicc2  24117  volsup  24151  uniioovol  24174  uniioombllem3a  24179  uniioombllem3  24180  uniioombllem4  24181  uniioombllem5  24182  uniioombl  24184  mbfdm  24221  ismbfcn  24224  mbfres  24239  mbfimaopnlem  24250  cncombf  24253  limccnp  24483  dvcobr  24537  dvcof  24539  dvcjbr  24540  dvcj  24541  dvmptco  24563  dvlip2  24586  itgsubstlem  24639  coecj  24862  pserulm  25004  jensenlem2  25559  jensen  25560  amgmlem  25561  gamf  25614  dchrinv  25831  motcgrg  26324  vsfval  28404  imsdf  28460  lnocoi  28528  hocofi  29537  homco1  29572  homco2  29748  hmopco  29794  kbass2  29888  kbass5  29891  opsqrlem1  29911  opsqrlem6  29916  pjinvari  29962  fmptco1f1o  30372  fcobij  30452  fcobijfs  30453  mbfmco  31517  dstfrvclim1  31730  reprpmtf1o  31892  subfacp1lem5  32426  mrsubco  32763  mclsppslem  32825  circum  32912  mblfinlem2  34924  mbfresfi  34932  ftc1anclem5  34965  ghomco  35163  rngohomco  35246  tendococl  37902  mapco2g  39304  diophrw  39349  hausgraph  39805  sblpnf  40635  fcoss  41466  limccog  41894  mbfres2cn  42236  volioof  42266  volioofmpt  42273  voliooicof  42275  stoweidlem31  42310  stoweidlem59  42338  subsaliuncllem  42634  sge0resrnlem  42679  hoicvr  42824  ovolval2lem  42919  ovolval2  42920  ovolval3  42923  ovolval4lem1  42925  ovolval5lem3  42930  isomushgr  43985  mgmhmco  44062  amgmwlem  44897
  Copyright terms: Public domain W3C validator