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

Theorem fco 5954
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 5791 . . 3 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
2 df-f 5791 . . 3 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
3 fnco 5896 . . . . . . 7 ((𝐹 Fn 𝐵𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴)
433expib 1259 . . . . . 6 (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
54adantr 479 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → (𝐹𝐺) Fn 𝐴))
6 rncoss 5291 . . . . . . 7 ran (𝐹𝐺) ⊆ ran 𝐹
7 sstr 3572 . . . . . . 7 ((ran (𝐹𝐺) ⊆ ran 𝐹 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
86, 7mpan 701 . . . . . 6 (ran 𝐹𝐶 → ran (𝐹𝐺) ⊆ 𝐶)
98adantl 480 . . . . 5 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ran (𝐹𝐺) ⊆ 𝐶)
105, 9jctird 564 . . . 4 ((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶)))
1110imp 443 . . 3 (((𝐹 Fn 𝐵 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
121, 2, 11syl2anb 494 . 2 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
13 df-f 5791 . 2 ((𝐹𝐺):𝐴𝐶 ↔ ((𝐹𝐺) Fn 𝐴 ∧ ran (𝐹𝐺) ⊆ 𝐶))
1412, 13sylibr 222 1 ((𝐹:𝐵𝐶𝐺:𝐴𝐵) → (𝐹𝐺):𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3536  ran crn 5026  ccom 5029   Fn wfn 5782  wf 5783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-fun 5789  df-fn 5790  df-f 5791
This theorem is referenced by:  fco2  5955  f1co  6005  foco  6020  mapen  7983  fsuppco2  8165  mapfienlem1  8167  mapfienlem3  8169  mapfien  8170  unxpwdom2  8350  wemapwe  8451  cofsmo  8948  cfcoflem  8951  isf34lem7  9058  isf34lem6  9059  canthp1lem2  9328  inar1  9450  addnqf  9623  mulnqf  9624  axdc4uzlem  12596  seqf1olem2  12655  wrdco  13371  lenco  13372  lo1o1  14054  o1co  14108  caucvgrlem2  14196  fsumcl2lem  14252  fsumadd  14260  fsummulc2  14301  fsumrelem  14323  supcvg  14370  fprodcl2lem  14462  fprodmul  14472  fproddiv  14473  fprodn0  14491  algcvg  15070  cofucl  16314  setccatid  16500  estrccatid  16538  funcestrcsetclem9  16554  funcsetcestrclem9  16569  yonedalem3b  16685  mhmco  17128  pwsco1mhm  17136  pwsco2mhm  17137  gsumwmhm  17148  f1omvdconj  17632  pmtrfinv  17647  symgtrinv  17658  psgnunilem1  17679  gsumval3lem1  18072  gsumval3lem2  18073  gsumval3  18074  gsumzcl2  18077  gsumzf1o  18079  gsumzaddlem  18087  gsumzmhm  18103  gsumzoppg  18110  gsumzinv  18111  gsumsub  18114  dprdf1o  18197  ablfaclem2  18251  psrass1lem  19141  psrnegcl  19160  coe1f2  19343  cnfldds  19520  dsmmbas2  19839  f1lindf  19919  lindfmm  19924  cpmadumatpolylem1  20444  cnco  20819  cnpco  20820  lmcnp  20857  cnmpt11  21215  cnmpt21  21223  qtopcn  21266  fmco  21514  flfcnp  21557  tsmsf1o  21697  tsmsmhm  21698  tsmssub  21701  imasdsf1olem  21926  comet  22066  nrmmetd  22127  isngp2  22149  isngp3  22150  tngngp2  22201  cnmet  22314  cnfldms  22318  cncfco  22446  cnfldcusp  22875  ovolfioo  22957  ovolficc  22958  ovolfsf  22961  ovollb  22968  ovolctb  22979  ovolicc2lem4  23009  ovolicc2  23011  volsup  23045  uniioovol  23067  uniioombllem3a  23072  uniioombllem3  23073  uniioombllem4  23074  uniioombllem5  23075  uniioombl  23077  mbfdm  23115  ismbfcn  23118  mbfres  23131  mbfimaopnlem  23142  cncombf  23145  limccnp  23375  dvcobr  23429  dvcof  23431  dvcjbr  23432  dvcj  23433  dvmptco  23455  dvlip2  23476  itgsubstlem  23529  coecj  23752  pserulm  23894  jensenlem2  24428  jensen  24429  amgmlem  24430  gamf  24483  dchrinv  24700  motcgrg  25154  vsfval  26655  imsdf  26722  lnocoi  26799  hocofi  27812  homco1  27847  homco2  28023  hmopco  28069  kbass2  28163  kbass5  28166  opsqrlem1  28186  opsqrlem6  28191  pjinvari  28237  fcobij  28691  fcobijfs  28692  mbfmco  29456  dstfrvclim1  29669  subfacp1lem5  30223  mrsubco  30475  mclsppslem  30537  circum  30625  mblfinlem2  32417  mbfresfi  32426  ftc1anclem5  32459  ghomco  32660  rngohomco  32743  tendococl  34878  mapco2g  36095  diophrw  36140  hausgraph  36609  sblpnf  37331  fcoss  38197  fcod  38219  limccog  38488  mbfres2cn  38651  volioof  38681  volioofmpt  38688  voliooicof  38690  stoweidlem31  38725  stoweidlem59  38753  subsaliuncllem  39052  sge0resrnlem  39097  hoicvr  39239  ovolval2lem  39334  ovolval2  39335  ovolval3  39338  ovolval4lem1  39340  ovolval5lem3  39345  mgmhmco  41590  amgmwlem  42317
  Copyright terms: Public domain W3C validator