Theorem fco 6058

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 5892	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 5892	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 5999	. . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)
4	3	3expib 1268	. . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
5	4	adantr 481	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
6		rncoss 5386	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3611	. . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
8	6, 7	mpan 706	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
9	8	adantl 482	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
10	5, 9	jctird 567	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)))
11	10	imp 445	. . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
12	1, 2, 11	syl2anb 496	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
13		df-f 5892	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 224	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 384   ⊆ wss 3574  ran crn 5115   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  fco2  6059  f1co  6110  foco  6125  mapen  8124  fsuppco2  8308  mapfienlem1  8310  mapfienlem3  8312  mapfien  8313  unxpwdom2  8493  wemapwe  8594  cofsmo  9091  cfcoflem  9094  isf34lem7  9201  isf34lem6  9202  canthp1lem2  9475  inar1  9597  addnqf  9770  mulnqf  9771  axdc4uzlem  12782  seqf1olem2  12841  wrdco  13577  lenco  13578  lo1o1  14263  o1co  14317  caucvgrlem2  14405  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumrelem  14539  supcvg  14588  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodn0  14709  algcvg  15289  cofucl  16548  setccatid  16734  estrccatid  16772  funcestrcsetclem9  16788  funcsetcestrclem9  16803  yonedalem3b  16919  mhmco  17362  pwsco1mhm  17370  pwsco2mhm  17371  gsumwmhm  17382  f1omvdconj  17866  pmtrfinv  17881  symgtrinv  17892  psgnunilem1  17913  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumzmhm  18337  gsumzoppg  18344  gsumzinv  18345  gsumsub  18348  dprdf1o  18431  ablfaclem2  18485  psrass1lem  19377  psrnegcl  19396  coe1f2  19579  cnfldds  19756  dsmmbas2  20081  f1lindf  20161  lindfmm  20166  cpmadumatpolylem1  20686  cnco  21070  cnpco  21071  lmcnp  21108  cnmpt11  21466  cnmpt21  21474  qtopcn  21517  fmco  21765  flfcnp  21808  tsmsf1o  21948  tsmsmhm  21949  tsmssub  21952  imasdsf1olem  22178  comet  22318  nrmmetd  22379  isngp2  22401  isngp3  22402  tngngp2  22456  cnmet  22575  cnfldms  22579  cncfco  22710  cnfldcusp  23153  ovolfioo  23236  ovolficc  23237  ovolfsf  23240  ovollb  23247  ovolctb  23258  ovolicc2lem4  23288  ovolicc2  23290  volsup  23324  uniioovol  23347  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  mbfdm  23395  ismbfcn  23398  mbfres  23411  mbfimaopnlem  23422  cncombf  23425  limccnp  23655  dvcobr  23709  dvcof  23711  dvcjbr  23712  dvcj  23713  dvmptco  23735  dvlip2  23758  itgsubstlem  23811  coecj  24034  pserulm  24176  jensenlem2  24714  jensen  24715  amgmlem  24716  gamf  24769  dchrinv  24986  motcgrg  25439  vsfval  27488  imsdf  27544  lnocoi  27612  hocofi  28625  homco1  28660  homco2  28836  hmopco  28882  kbass2  28976  kbass5  28979  opsqrlem1  28999  opsqrlem6  29004  pjinvari  29050  fmptco1f1o  29434  fcobij  29500  fcobijfs  29501  mbfmco  30326  dstfrvclim1  30539  reprpmtf1o  30704  subfacp1lem5  31166  mrsubco  31418  mclsppslem  31480  circum  31568  mblfinlem2  33447  mbfresfi  33456  ftc1anclem5  33489  ghomco  33690  rngohomco  33773  tendococl  36060  mapco2g  37277  diophrw  37322  hausgraph  37790  sblpnf  38509  fcoss  39402  fcod  39424  limccog  39852  mbfres2cn  40174  volioof  40204  volioofmpt  40211  voliooicof  40213  stoweidlem31  40248  stoweidlem59  40276  subsaliuncllem  40575  sge0resrnlem  40620  hoicvr  40762  ovolval2lem  40857  ovolval2  40858  ovolval3  40861  ovolval4lem1  40863  ovolval5lem3  40868  mgmhmco  41801  amgmwlem  42548