Theorem fco 6526

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 6354	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 6354	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6460	. . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)
4	3	3expib 1118	. . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
5	4	adantr 483	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
6		rncoss 5838	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3975	. . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
8	6, 7	mpan 688	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
9	8	adantl 484	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
10	5, 9	jctird 529	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)))
11	10	imp 409	. . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
12	1, 2, 11	syl2anb 599	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
13		df-f 6354	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 236	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3936  ran crn 5551   ∘ ccom 5554   Fn wfn 6345  ⟶wf 6346

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 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322

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 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060  df-opab 5122  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-fun 6352  df-fn 6353  df-f 6354

This theorem is referenced by:  fcod  6527  fco2  6528  f1co  6580  foco  6597  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  41465  limccog  41893  mbfres2cn  42235  volioof  42265  volioofmpt  42272  voliooicof  42274  stoweidlem31  42309  stoweidlem59  42337  subsaliuncllem  42633  sge0resrnlem  42678  hoicvr  42823  ovolval2lem  42918  ovolval2  42919  ovolval3  42922  ovolval4lem1  42924  ovolval5lem3  42929  isomushgr  43984  mgmhmco  44061  amgmwlem  44896