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

Theorem fco 6025
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 5861 . . 3 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
2 df-f 5861 . . 3 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
3 fnco 5967 . . . . . . 7 ((𝐹 Fn 𝐵𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴)
433expib 1265 . . . . . 6 (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
54adantr 481 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
6 rncoss 5356 . . . . . . 7 ran (𝐹𝐺) ⊆ ran 𝐹
7 sstr 3596 . . . . . . 7 ((ran (𝐹𝐺) ⊆ ran 𝐹 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
86, 7mpan 705 . . . . . 6 (ran 𝐹𝐶 → ran (𝐹𝐺) ⊆ 𝐶)
98adantl 482 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
105, 9jctird 566 . . . 4 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶)))
1110imp 445 . . 3 (((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
121, 2, 11syl2anb 496 . 2 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
13 df-f 5861 . 2 ((𝐹𝐺):𝐴𝐶 ↔ ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
1412, 13sylibr 224 1 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wss 3560  ran crn 5085  ccom 5088   Fn wfn 5852  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-fun 5859  df-fn 5860  df-f 5861
This theorem is referenced by:  fco2  6026  f1co  6077  foco  6092  mapen  8084  fsuppco2  8268  mapfienlem1  8270  mapfienlem3  8272  mapfien  8273  unxpwdom2  8453  wemapwe  8554  cofsmo  9051  cfcoflem  9054  isf34lem7  9161  isf34lem6  9162  canthp1lem2  9435  inar1  9557  addnqf  9730  mulnqf  9731  axdc4uzlem  12738  seqf1olem2  12797  wrdco  13530  lenco  13531  lo1o1  14213  o1co  14267  caucvgrlem2  14355  fsumcl2lem  14411  fsumadd  14419  fsummulc2  14463  fsumrelem  14485  supcvg  14532  fprodcl2lem  14624  fprodmul  14634  fproddiv  14635  fprodn0  14653  algcvg  15232  cofucl  16488  setccatid  16674  estrccatid  16712  funcestrcsetclem9  16728  funcsetcestrclem9  16743  yonedalem3b  16859  mhmco  17302  pwsco1mhm  17310  pwsco2mhm  17311  gsumwmhm  17322  f1omvdconj  17806  pmtrfinv  17821  symgtrinv  17832  psgnunilem1  17853  gsumval3lem1  18246  gsumval3lem2  18247  gsumval3  18248  gsumzcl2  18251  gsumzf1o  18253  gsumzaddlem  18261  gsumzmhm  18277  gsumzoppg  18284  gsumzinv  18285  gsumsub  18288  dprdf1o  18371  ablfaclem2  18425  psrass1lem  19317  psrnegcl  19336  coe1f2  19519  cnfldds  19696  dsmmbas2  20021  f1lindf  20101  lindfmm  20106  cpmadumatpolylem1  20626  cnco  21010  cnpco  21011  lmcnp  21048  cnmpt11  21406  cnmpt21  21414  qtopcn  21457  fmco  21705  flfcnp  21748  tsmsf1o  21888  tsmsmhm  21889  tsmssub  21892  imasdsf1olem  22118  comet  22258  nrmmetd  22319  isngp2  22341  isngp3  22342  tngngp2  22396  cnmet  22515  cnfldms  22519  cncfco  22650  cnfldcusp  23093  ovolfioo  23176  ovolficc  23177  ovolfsf  23180  ovollb  23187  ovolctb  23198  ovolicc2lem4  23228  ovolicc2  23230  volsup  23264  uniioovol  23287  uniioombllem3a  23292  uniioombllem3  23293  uniioombllem4  23294  uniioombllem5  23295  uniioombl  23297  mbfdm  23335  ismbfcn  23338  mbfres  23351  mbfimaopnlem  23362  cncombf  23365  limccnp  23595  dvcobr  23649  dvcof  23651  dvcjbr  23652  dvcj  23653  dvmptco  23675  dvlip2  23696  itgsubstlem  23749  coecj  23972  pserulm  24114  jensenlem2  24648  jensen  24649  amgmlem  24650  gamf  24703  dchrinv  24920  motcgrg  25373  vsfval  27376  imsdf  27432  lnocoi  27500  hocofi  28513  homco1  28548  homco2  28724  hmopco  28770  kbass2  28864  kbass5  28867  opsqrlem1  28887  opsqrlem6  28892  pjinvari  28938  fcobij  29384  fcobijfs  29385  mbfmco  30149  dstfrvclim1  30362  subfacp1lem5  30927  mrsubco  31179  mclsppslem  31241  circum  31329  mblfinlem2  33118  mbfresfi  33127  ftc1anclem5  33160  ghomco  33361  rngohomco  33444  tendococl  35579  mapco2g  36796  diophrw  36841  hausgraph  37310  sblpnf  38030  fcoss  38911  fcod  38933  limccog  39288  mbfres2cn  39511  volioof  39541  volioofmpt  39548  voliooicof  39550  stoweidlem31  39585  stoweidlem59  39613  subsaliuncllem  39912  sge0resrnlem  39957  hoicvr  40099  ovolval2lem  40194  ovolval2  40195  ovolval3  40198  ovolval4lem1  40200  ovolval5lem3  40205  mgmhmco  41119  amgmwlem  41881
  Copyright terms: Public domain W3C validator