Theorem fco 6096

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 5930	. . 3 ⊢ (𝐹:𝐵⟶𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶))
2		df-f 5930	. . 3 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
3		fnco 6037	. . . . . . 7 ⊢ ((𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴)
4	3	3expib 1287	. . . . . 6 ⊢ (𝐹 Fn 𝐵 → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
5	4	adantr 480	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐴))
6		rncoss 5418	. . . . . . 7 ⊢ ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹
7		sstr 3644	. . . . . . 7 ⊢ ((ran (𝐹 ∘ 𝐺) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
8	6, 7	mpan 706	. . . . . 6 ⊢ (ran 𝐹 ⊆ 𝐶 → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
9	8	adantl 481	. . . . 5 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ran (𝐹 ∘ 𝐺) ⊆ 𝐶)
10	5, 9	jctird 566	. . . 4 ⊢ ((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) → ((𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶)))
11	10	imp 444	. . 3 ⊢ (((𝐹 Fn 𝐵 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
12	1, 2, 11	syl2anb 495	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
13		df-f 5930	. 2 ⊢ ((𝐹 ∘ 𝐺):𝐴⟶𝐶 ↔ ((𝐹 ∘ 𝐺) Fn 𝐴 ∧ ran (𝐹 ∘ 𝐺) ⊆ 𝐶))
14	12, 13	sylibr 224	1 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3607  ran crn 5144   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930

This theorem is referenced by:  fco2  6097  f1co  6148  foco  6163  mapen  8165  fsuppco2  8349  mapfienlem1  8351  mapfienlem3  8353  mapfien  8354  unxpwdom2  8534  wemapwe  8632  cofsmo  9129  cfcoflem  9132  isf34lem7  9239  isf34lem6  9240  canthp1lem2  9513  inar1  9635  addnqf  9808  mulnqf  9809  axdc4uzlem  12822  seqf1olem2  12881  wrdco  13623  lenco  13624  lo1o1  14307  o1co  14361  caucvgrlem2  14449  fsumcl2lem  14506  fsumadd  14514  fsummulc2  14560  fsumrelem  14583  supcvg  14632  fprodcl2lem  14724  fprodmul  14734  fproddiv  14735  fprodn0  14753  algcvg  15336  cofucl  16595  setccatid  16781  estrccatid  16819  funcestrcsetclem9  16835  funcsetcestrclem9  16850  yonedalem3b  16966  mhmco  17409  pwsco1mhm  17417  pwsco2mhm  17418  gsumwmhm  17429  f1omvdconj  17912  pmtrfinv  17927  symgtrinv  17938  psgnunilem1  17959  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  gsumzcl2  18357  gsumzf1o  18359  gsumzaddlem  18367  gsumzmhm  18383  gsumzoppg  18390  gsumzinv  18391  gsumsub  18394  dprdf1o  18477  ablfaclem2  18531  psrass1lem  19425  psrnegcl  19444  coe1f2  19627  cnfldds  19804  dsmmbas2  20129  f1lindf  20209  lindfmm  20214  cpmadumatpolylem1  20734  cnco  21118  cnpco  21119  lmcnp  21156  cnmpt11  21514  cnmpt21  21522  qtopcn  21565  fmco  21812  flfcnp  21855  tsmsf1o  21995  tsmsmhm  21996  tsmssub  21999  imasdsf1olem  22225  comet  22365  nrmmetd  22426  isngp2  22448  isngp3  22449  tngngp2  22503  cnmet  22622  cnfldms  22626  cncfco  22757  cnfldcusp  23199  ovolfioo  23282  ovolficc  23283  ovolfsf  23286  ovollb  23293  ovolctb  23304  ovolicc2lem4  23334  ovolicc2  23336  volsup  23370  uniioovol  23393  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  uniioombl  23403  mbfdm  23440  ismbfcn  23443  mbfres  23456  mbfimaopnlem  23467  cncombf  23470  limccnp  23700  dvcobr  23754  dvcof  23756  dvcjbr  23757  dvcj  23758  dvmptco  23780  dvlip2  23803  itgsubstlem  23856  coecj  24079  pserulm  24221  jensenlem2  24759  jensen  24760  amgmlem  24761  gamf  24814  dchrinv  25031  motcgrg  25484  vsfval  27616  imsdf  27672  lnocoi  27740  hocofi  28753  homco1  28788  homco2  28964  hmopco  29010  kbass2  29104  kbass5  29107  opsqrlem1  29127  opsqrlem6  29132  pjinvari  29178  fmptco1f1o  29562  fcobij  29628  fcobijfs  29629  mbfmco  30454  dstfrvclim1  30667  reprpmtf1o  30832  subfacp1lem5  31292  mrsubco  31544  mclsppslem  31606  circum  31694  mblfinlem2  33577  mbfresfi  33586  ftc1anclem5  33619  ghomco  33820  rngohomco  33903  tendococl  36377  mapco2g  37594  diophrw  37639  hausgraph  38107  sblpnf  38826  fcoss  39716  fcod  39738  limccog  40170  mbfres2cn  40492  volioof  40522  volioofmpt  40529  voliooicof  40531  stoweidlem31  40566  stoweidlem59  40594  subsaliuncllem  40893  sge0resrnlem  40938  hoicvr  41083  ovolval2lem  41178  ovolval2  41179  ovolval3  41182  ovolval4lem1  41184  ovolval5lem3  41189  mgmhmco  42126  amgmwlem  42876