Theorem fco 6533

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 6361	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 6361	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6467	. . . . . . 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 5845	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3977	. . . . . . 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 6361	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 236	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3938  ran crn 5558   ∘ ccom 5561   Fn wfn 6352  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  fcod  6534  fco2  6535  f1co  6587  foco  6604  mapen  8683  fsuppco2  8868  mapfienlem1  8870  mapfienlem3  8872  mapfien  8873  unxpwdom2  9054  wemapwe  9162  cofsmo  9693  cfcoflem  9696  isf34lem7  9803  isf34lem6  9804  canthp1lem2  10077  inar1  10199  addnqf  10372  mulnqf  10373  axdc4uzlem  13354  seqf1olem2  13413  wrdco  14195  lenco  14196  lo1o1  14891  o1co  14945  caucvgrlem2  15033  fsumcl2lem  15090  fsumadd  15098  fsummulc2  15141  fsumrelem  15164  supcvg  15213  fprodcl2lem  15306  fprodmul  15316  fproddiv  15317  fprodn0  15335  algcvg  15922  cofucl  17160  setccatid  17346  estrccatid  17384  funcestrcsetclem9  17400  funcsetcestrclem9  17415  yonedalem3b  17531  mhmco  17990  pwsco1mhm  17998  pwsco2mhm  17999  gsumwmhm  18012  efmndcl  18049  f1omvdconj  18576  pmtrfinv  18591  symgtrinv  18602  psgnunilem1  18623  gsumval3lem1  19027  gsumval3lem2  19028  gsumval3  19029  gsumzcl2  19032  gsumzf1o  19034  gsumzaddlem  19043  gsumzmhm  19059  gsumzoppg  19066  gsumzinv  19067  gsumsub  19070  dprdf1o  19156  ablfaclem2  19210  psrass1lem  20159  psrnegcl  20178  coe1f2  20379  cnfldds  20557  dsmmbas2  20883  f1lindf  20968  lindfmm  20973  cpmadumatpolylem1  21491  cnco  21876  cnpco  21877  lmcnp  21914  cnmpt11  22273  cnmpt21  22281  qtopcn  22324  fmco  22571  flfcnp  22614  tsmsf1o  22755  tsmsmhm  22756  tsmssub  22759  imasdsf1olem  22985  comet  23125  nrmmetd  23186  isngp2  23208  isngp3  23209  tngngp2  23263  cnmet  23382  cnfldms  23386  cncfco  23517  cnfldcusp  23962  ovolfioo  24070  ovolficc  24071  ovolfsf  24074  ovollb  24082  ovolctb  24093  ovolicc2lem4  24123  ovolicc2  24125  volsup  24159  uniioovol  24182  uniioombllem3a  24187  uniioombllem3  24188  uniioombllem4  24189  uniioombllem5  24190  uniioombl  24192  mbfdm  24229  ismbfcn  24232  mbfres  24247  mbfimaopnlem  24258  cncombf  24261  limccnp  24491  dvcobr  24545  dvcof  24547  dvcjbr  24548  dvcj  24549  dvmptco  24571  dvlip2  24594  itgsubstlem  24647  coecj  24870  pserulm  25012  jensenlem2  25567  jensen  25568  amgmlem  25569  gamf  25622  dchrinv  25839  motcgrg  26332  vsfval  28412  imsdf  28468  lnocoi  28536  hocofi  29545  homco1  29580  homco2  29756  hmopco  29802  kbass2  29896  kbass5  29899  opsqrlem1  29919  opsqrlem6  29924  pjinvari  29970  fmptco1f1o  30380  fcobij  30460  fcobijfs  30461  mbfmco  31524  dstfrvclim1  31737  reprpmtf1o  31899  subfacp1lem5  32433  mrsubco  32770  mclsppslem  32832  circum  32919  mblfinlem2  34932  mbfresfi  34940  ftc1anclem5  34973  ghomco  35171  rngohomco  35254  tendococl  37910  mapco2g  39318  diophrw  39363  hausgraph  39819  sblpnf  40649  fcoss  41480  limccog  41908  mbfres2cn  42250  volioof  42279  volioofmpt  42286  voliooicof  42288  stoweidlem31  42323  stoweidlem59  42351  subsaliuncllem  42647  sge0resrnlem  42692  hoicvr  42837  ovolval2lem  42932  ovolval2  42933  ovolval3  42936  ovolval4lem1  42938  ovolval5lem3  42943  isomushgr  43998  mgmhmco  44075  amgmwlem  44910