Theorem fco 6516

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 6339	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 6339	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6448	. . . . . . 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 5813	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3900	. . . . . . 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 6339	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 237	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3858  ran crn 5525   ∘ ccom 5528   Fn wfn 6330  ⟶wf 6331

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 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-fun 6337  df-fn 6338  df-f 6339

This theorem is referenced by:  fcod  6517  fco2  6518  f1co  6571  foco  6588  mapen  8703  fsuppco2  8900  mapfienlem1  8902  unxpwdom2  9085  wemapwe  9193  cfcoflem  9732  isf34lem7  9839  isf34lem6  9840  inar1  10235  addnqf  10408  mulnqf  10409  axdc4uzlem  13400  seqf1olem2  13460  wrdco  14240  lenco  14241  lo1o1  14937  o1co  14991  caucvgrlem2  15079  fsumcl2lem  15136  fsumadd  15144  fsummulc2  15187  fsumrelem  15210  supcvg  15259  fprodcl2lem  15352  fprodmul  15362  fproddiv  15363  fprodn0  15381  algcvg  15972  cofucl  17217  setccatid  17410  estrccatid  17448  funcestrcsetclem9  17464  funcsetcestrclem9  17479  yonedalem3b  17595  mhmco  18054  pwsco1mhm  18062  pwsco2mhm  18063  gsumwmhm  18076  efmndcl  18113  f1omvdconj  18641  pmtrfinv  18656  symgtrinv  18667  psgnunilem1  18688  gsumval3lem1  19093  gsumval3  19095  gsumzcl2  19098  gsumzf1o  19100  gsumzaddlem  19109  gsumzmhm  19125  gsumzoppg  19132  gsumzinv  19133  gsumsub  19136  dprdf1o  19222  ablfaclem2  19276  cnfldds  20176  dsmmbas2  20502  f1lindf  20587  lindfmm  20592  psrass1lemOLD  20702  psrnegcl  20724  coe1f2  20933  cpmadumatpolylem1  21581  cnco  21966  cnpco  21967  lmcnp  22004  cnmpt11  22363  cnmpt21  22371  qtopcn  22414  fmco  22661  flfcnp  22704  tsmsf1o  22845  tsmsmhm  22846  tsmssub  22849  imasdsf1olem  23075  nrmmetd  23276  isngp2  23299  isngp3  23300  tngngp2  23354  cnmet  23473  cnfldms  23477  cncfco  23608  cnfldcusp  24057  ovolfioo  24167  ovolficc  24168  ovolfsf  24171  ovollb  24179  ovolctb  24190  ovolicc2lem4  24220  ovolicc2  24222  volsup  24256  uniioovol  24279  uniioombllem3a  24284  uniioombllem3  24285  uniioombllem4  24286  uniioombllem5  24287  uniioombl  24289  mbfdm  24326  ismbfcn  24329  mbfres  24344  mbfimaopnlem  24355  cncombf  24358  limccnp  24590  dvcobr  24645  dvcof  24647  dvcjbr  24648  dvcj  24649  dvmptco  24671  dvlip2  24694  itgsubstlem  24747  coecj  24974  pserulm  25116  jensenlem2  25672  jensen  25673  amgmlem  25674  gamf  25727  dchrinv  25944  motcgrg  26437  vsfval  28515  imsdf  28571  lnocoi  28639  hocofi  29648  homco1  29683  homco2  29859  hmopco  29905  kbass2  29999  kbass5  30002  opsqrlem1  30022  opsqrlem6  30027  pjinvari  30073  fmptco1f1o  30490  fcobij  30581  fcobijfs  30582  mbfmco  31750  dstfrvclim1  31963  reprpmtf1o  32125  mrsubco  32999  mclsppslem  33061  circum  33148  mblfinlem2  35375  mbfresfi  35383  ftc1anclem5  35414  ghomco  35609  rngohomco  35692  tendococl  38348  mapco2g  40028  diophrw  40073  hausgraph  40529  sblpnf  41387  fcoss  42209  limccog  42628  mbfres2cn  42966  volioof  42995  volioofmpt  43002  voliooicof  43004  stoweidlem31  43039  stoweidlem59  43067  subsaliuncllem  43363  sge0resrnlem  43408  hoicvr  43553  ovolval2lem  43648  ovolval2  43649  ovolval3  43652  ovolval4lem1  43654  ovolval5lem3  43659  isomushgr  44711  mgmhmco  44788  amgmwlem  45721