Theorem fco 6505

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 6328	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 6328	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6437	. . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)
4	3	3expib 1119	. . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
5	4	adantr 484	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
6		rncoss 5808	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3923	. . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
8	6, 7	mpan 689	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
9	8	adantl 485	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
10	5, 9	jctird 530	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)))
11	10	imp 410	. . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
12	1, 2, 11	syl2anb 600	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
13		df-f 6328	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 237	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3881  ran crn 5520   ∘ ccom 5523   Fn wfn 6319  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  fcod  6506  fco2  6507  f1co  6560  foco  6577  mapen  8665  fsuppco2  8850  mapfienlem1  8852  mapfienlem3  8854  mapfien  8855  unxpwdom2  9036  wemapwe  9144  cofsmo  9680  cfcoflem  9683  isf34lem7  9790  isf34lem6  9791  canthp1lem2  10064  inar1  10186  addnqf  10359  mulnqf  10360  axdc4uzlem  13346  seqf1olem2  13406  wrdco  14184  lenco  14185  lo1o1  14881  o1co  14935  caucvgrlem2  15023  fsumcl2lem  15080  fsumadd  15088  fsummulc2  15131  fsumrelem  15154  supcvg  15203  fprodcl2lem  15296  fprodmul  15306  fproddiv  15307  fprodn0  15325  algcvg  15910  cofucl  17150  setccatid  17336  estrccatid  17374  funcestrcsetclem9  17390  funcsetcestrclem9  17405  yonedalem3b  17521  mhmco  17980  pwsco1mhm  17988  pwsco2mhm  17989  gsumwmhm  18002  efmndcl  18039  f1omvdconj  18566  pmtrfinv  18581  symgtrinv  18592  psgnunilem1  18613  gsumval3lem1  19018  gsumval3lem2  19019  gsumval3  19020  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumzmhm  19050  gsumzoppg  19057  gsumzinv  19058  gsumsub  19061  dprdf1o  19147  ablfaclem2  19201  cnfldds  20101  dsmmbas2  20426  f1lindf  20511  lindfmm  20516  psrass1lem  20615  psrnegcl  20634  coe1f2  20838  cpmadumatpolylem1  21486  cnco  21871  cnpco  21872  lmcnp  21909  cnmpt11  22268  cnmpt21  22276  qtopcn  22319  fmco  22566  flfcnp  22609  tsmsf1o  22750  tsmsmhm  22751  tsmssub  22754  imasdsf1olem  22980  nrmmetd  23181  isngp2  23203  isngp3  23204  tngngp2  23258  cnmet  23377  cnfldms  23381  cncfco  23512  cnfldcusp  23961  ovolfioo  24071  ovolficc  24072  ovolfsf  24075  ovollb  24083  ovolctb  24094  ovolicc2lem4  24124  ovolicc2  24126  volsup  24160  uniioovol  24183  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombl  24193  mbfdm  24230  ismbfcn  24233  mbfres  24248  mbfimaopnlem  24259  cncombf  24262  limccnp  24494  dvcobr  24549  dvcof  24551  dvcjbr  24552  dvcj  24553  dvmptco  24575  dvlip2  24598  itgsubstlem  24651  coecj  24875  pserulm  25017  jensenlem2  25573  jensen  25574  amgmlem  25575  gamf  25628  dchrinv  25845  motcgrg  26338  vsfval  28416  imsdf  28472  lnocoi  28540  hocofi  29549  homco1  29584  homco2  29760  hmopco  29806  kbass2  29900  kbass5  29903  opsqrlem1  29923  opsqrlem6  29928  pjinvari  29974  fmptco1f1o  30392  fcobij  30484  fcobijfs  30485  mbfmco  31632  dstfrvclim1  31845  reprpmtf1o  32007  subfacp1lem5  32544  mrsubco  32881  mclsppslem  32943  circum  33030  mblfinlem2  35095  mbfresfi  35103  ftc1anclem5  35134  ghomco  35329  rngohomco  35412  tendococl  38068  mapco2g  39655  diophrw  39700  hausgraph  40156  sblpnf  41014  fcoss  41839  limccog  42262  mbfres2cn  42600  volioof  42629  volioofmpt  42636  voliooicof  42638  stoweidlem31  42673  stoweidlem59  42701  subsaliuncllem  42997  sge0resrnlem  43042  hoicvr  43187  ovolval2lem  43282  ovolval2  43283  ovolval3  43286  ovolval4lem1  43288  ovolval5lem3  43293  isomushgr  44344  mgmhmco  44421  amgmwlem  45330