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

Theorem fco 5971
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 5808 . . 3 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
2 df-f 5808 . . 3 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
3 fnco 5913 . . . . . . 7 ((𝐹 Fn 𝐵𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴)
433expib 1260 . . . . . 6 (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
54adantr 480 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
6 rncoss 5307 . . . . . . 7 ran (𝐹𝐺) ⊆ ran 𝐹
7 sstr 3576 . . . . . . 7 ((ran (𝐹𝐺) ⊆ ran 𝐹 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
86, 7mpan 702 . . . . . 6 (ran 𝐹𝐶 → ran (𝐹𝐺) ⊆ 𝐶)
98adantl 481 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
105, 9jctird 565 . . . 4 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶)))
1110imp 444 . . 3 (((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
121, 2, 11syl2anb 495 . 2 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
13 df-f 5808 . 2 ((𝐹𝐺):𝐴𝐶 ↔ ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
1412, 13sylibr 223 1 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wss 3540  ran crn 5039  ccom 5042   Fn wfn 5799  wf 5800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808
This theorem is referenced by:  fco2  5972  f1co  6023  foco  6038  mapen  8009  fsuppco2  8191  mapfienlem1  8193  mapfienlem3  8195  mapfien  8196  unxpwdom2  8376  wemapwe  8477  cofsmo  8974  cfcoflem  8977  isf34lem7  9084  isf34lem6  9085  canthp1lem2  9354  inar1  9476  addnqf  9649  mulnqf  9650  axdc4uzlem  12644  seqf1olem2  12703  wrdco  13428  lenco  13429  lo1o1  14111  o1co  14165  caucvgrlem2  14253  fsumcl2lem  14309  fsumadd  14317  fsummulc2  14358  fsumrelem  14380  supcvg  14427  fprodcl2lem  14519  fprodmul  14529  fproddiv  14530  fprodn0  14548  algcvg  15127  cofucl  16371  setccatid  16557  estrccatid  16595  funcestrcsetclem9  16611  funcsetcestrclem9  16626  yonedalem3b  16742  mhmco  17185  pwsco1mhm  17193  pwsco2mhm  17194  gsumwmhm  17205  f1omvdconj  17689  pmtrfinv  17704  symgtrinv  17715  psgnunilem1  17736  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  gsumzinv  18168  gsumsub  18171  dprdf1o  18254  ablfaclem2  18308  psrass1lem  19198  psrnegcl  19217  coe1f2  19400  cnfldds  19577  dsmmbas2  19900  f1lindf  19980  lindfmm  19985  cpmadumatpolylem1  20505  cnco  20880  cnpco  20881  lmcnp  20918  cnmpt11  21276  cnmpt21  21284  qtopcn  21327  fmco  21575  flfcnp  21618  tsmsf1o  21758  tsmsmhm  21759  tsmssub  21762  imasdsf1olem  21988  comet  22128  nrmmetd  22189  isngp2  22211  isngp3  22212  tngngp2  22266  cnmet  22385  cnfldms  22389  cncfco  22518  cnfldcusp  22961  ovolfioo  23043  ovolficc  23044  ovolfsf  23047  ovollb  23054  ovolctb  23065  ovolicc2lem4  23095  ovolicc2  23097  volsup  23131  uniioovol  23153  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  mbfdm  23201  ismbfcn  23204  mbfres  23217  mbfimaopnlem  23228  cncombf  23231  limccnp  23461  dvcobr  23515  dvcof  23517  dvcjbr  23518  dvcj  23519  dvmptco  23541  dvlip2  23562  itgsubstlem  23615  coecj  23838  pserulm  23980  jensenlem2  24514  jensen  24515  amgmlem  24516  gamf  24569  dchrinv  24786  motcgrg  25239  vsfval  26872  imsdf  26928  lnocoi  26996  hocofi  28009  homco1  28044  homco2  28220  hmopco  28266  kbass2  28360  kbass5  28363  opsqrlem1  28383  opsqrlem6  28388  pjinvari  28434  fcobij  28888  fcobijfs  28889  mbfmco  29653  dstfrvclim1  29866  subfacp1lem5  30420  mrsubco  30672  mclsppslem  30734  circum  30822  mblfinlem2  32617  mbfresfi  32626  ftc1anclem5  32659  ghomco  32860  rngohomco  32943  tendococl  35078  mapco2g  36295  diophrw  36340  hausgraph  36809  sblpnf  37531  fcoss  38397  fcod  38419  limccog  38687  mbfres2cn  38850  volioof  38880  volioofmpt  38887  voliooicof  38889  stoweidlem31  38924  stoweidlem59  38952  subsaliuncllem  39251  sge0resrnlem  39296  hoicvr  39438  ovolval2lem  39533  ovolval2  39534  ovolval3  39537  ovolval4lem1  39539  ovolval5lem3  39544  mgmhmco  41591  amgmwlem  42357
  Copyright terms: Public domain W3C validator