Theorem fco 6295

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

Step	Hyp	Ref	Expression
1		df-f 6127	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 6127	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6232	. . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)
4	3	3expib 1156	. . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
5	4	adantr 474	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
6		rncoss 5619	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3835	. . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
8	6, 7	mpan 681	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
9	8	adantl 475	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
10	5, 9	jctird 522	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)))
11	10	imp 397	. . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
12	1, 2, 11	syl2anb 591	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
13		df-f 6127	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 226	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 386   ⊆ wss 3798  ran crn 5343   ∘ ccom 5346   Fn wfn 6118  ⟶wf 6119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-fun 6125  df-fn 6126  df-f 6127

This theorem is referenced by:  fco2  6296  f1co  6348  foco  6365  mapen  8393  fsuppco2  8577  mapfienlem1  8579  mapfienlem3  8581  mapfien  8582  unxpwdom2  8762  wemapwe  8871  cofsmo  9406  cfcoflem  9409  isf34lem7  9516  isf34lem6  9517  canthp1lem2  9790  inar1  9912  addnqf  10085  mulnqf  10086  axdc4uzlem  13077  seqf1olem2  13135  wrdco  13952  lenco  13953  lo1o1  14640  o1co  14694  caucvgrlem2  14782  fsumcl2lem  14839  fsumadd  14847  fsummulc2  14890  fsumrelem  14913  supcvg  14962  fprodcl2lem  15053  fprodmul  15063  fproddiv  15064  fprodn0  15082  algcvg  15662  cofucl  16900  setccatid  17086  estrccatid  17124  funcestrcsetclem9  17141  funcsetcestrclem9  17156  yonedalem3b  17272  mhmco  17715  pwsco1mhm  17723  pwsco2mhm  17724  gsumwmhm  17736  f1omvdconj  18216  pmtrfinv  18231  symgtrinv  18242  psgnunilem1  18263  gsumval3lem1  18659  gsumval3lem2  18660  gsumval3  18661  gsumzcl2  18664  gsumzf1o  18666  gsumzaddlem  18674  gsumzmhm  18690  gsumzoppg  18697  gsumzinv  18698  gsumsub  18701  dprdf1o  18785  ablfaclem2  18839  psrass1lem  19738  psrnegcl  19757  coe1f2  19939  cnfldds  20116  dsmmbas2  20444  f1lindf  20528  lindfmm  20533  cpmadumatpolylem1  21056  cnco  21441  cnpco  21442  lmcnp  21479  cnmpt11  21837  cnmpt21  21845  qtopcn  21888  fmco  22135  flfcnp  22178  tsmsf1o  22318  tsmsmhm  22319  tsmssub  22322  imasdsf1olem  22548  comet  22688  nrmmetd  22749  isngp2  22771  isngp3  22772  tngngp2  22826  cnmet  22945  cnfldms  22949  cncfco  23080  cnfldcusp  23525  ovolfioo  23633  ovolficc  23634  ovolfsf  23637  ovollb  23645  ovolctb  23656  ovolicc2lem4  23686  ovolicc2  23688  volsup  23722  uniioovol  23745  uniioombllem3a  23750  uniioombllem3  23751  uniioombllem4  23752  uniioombllem5  23753  uniioombl  23755  mbfdm  23792  ismbfcn  23795  mbfres  23810  mbfimaopnlem  23821  cncombf  23824  limccnp  24054  dvcobr  24108  dvcof  24110  dvcjbr  24111  dvcj  24112  dvmptco  24134  dvlip2  24157  itgsubstlem  24210  coecj  24433  pserulm  24575  jensenlem2  25127  jensen  25128  amgmlem  25129  gamf  25182  dchrinv  25399  motcgrg  25856  vsfval  28032  imsdf  28088  lnocoi  28156  hocofi  29169  homco1  29204  homco2  29380  hmopco  29426  kbass2  29520  kbass5  29523  opsqrlem1  29543  opsqrlem6  29548  pjinvari  29594  fmptco1f1o  29972  fcobij  30037  fcobijfs  30038  mbfmco  30860  dstfrvclim1  31074  reprpmtf1o  31242  subfacp1lem5  31701  mrsubco  31953  mclsppslem  32015  circum  32101  mblfinlem2  33984  mbfresfi  33992  ftc1anclem5  34025  ghomco  34225  rngohomco  34308  tendococl  36840  mapco2g  38114  diophrw  38159  hausgraph  38626  sblpnf  39342  fcoss  40201  fcod  40221  limccog  40640  mbfres2cn  40961  volioof  40991  volioofmpt  40998  voliooicof  41000  stoweidlem31  41035  stoweidlem59  41063  subsaliuncllem  41359  sge0resrnlem  41404  hoicvr  41549  ovolval2lem  41644  ovolval2  41645  ovolval3  41648  ovolval4lem1  41650  ovolval5lem3  41655  isomushgr  42537  mgmhmco  42641  amgmwlem  43437