Theorem fssres 6697

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
fssres	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Proof of Theorem fssres

Step	Hyp	Ref	Expression
1		df-f 6493	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6612	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5957	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5887	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3940	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 690	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 613	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 652	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6493	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3899  ran crn 5622   ↾ cres 5623   Fn wfn 6484  ⟶wf 6485

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-fun 6491  df-fn 6492  df-f 6493

This theorem is referenced by:  fssresd  6698  fssres2  6699  fresin  6700  fresaun  6702  f1ssres  6734  resf1extb  7873  resf1ext2b  7874  f2ndf  8059  elmapssres  8800  pmresg  8803  ralxpmap  8829  mapunen  9069  fofinf1o  9226  fseqenlem1  9925  inar1  10676  gruima  10703  addnqf  10849  mulnqf  10850  fseq1p1m1  13508  injresinj  13701  seqf1olem2  13959  wrdred1  14477  rlimres  15475  lo1res  15476  vdwnnlem1  16917  fsets  17090  resmgmhm  18629  resmhm  18738  resghm  19154  gsumzres  19831  gsumzadd  19844  gsum2dlem2  19893  dpjidcl  19982  ablfac1eu  19997  abvres  20756  znf1o  21498  islindf4  21785  kgencn  23481  ptrescn  23564  hmeores  23696  tsmsres  24069  tsmsmhm  24071  tsmsadd  24072  xrge0gsumle  24759  xrge0tsms  24760  ovolicc2lem4  25458  limcdif  25814  limcflf  25819  limcmo  25820  dvres  25849  dvres3a  25852  aannenlem1  26273  logcn  26593  dvlog  26597  dvlog2  26599  logtayl  26606  dvatan  26882  atancn  26883  efrlim  26916  efrlimOLD  26917  amgm  26938  dchrelbas2  27185  redwlklem  29659  pthdivtx  29716  hhssabloilem  31252  hhssnv  31255  wrdres  32927  gsumpart  33048  xrge0tsmsd  33053  cntmeas  34250  eulerpartlemt  34395  eulerpartlemmf  34399  eulerpartlemgvv  34400  subiwrd  34409  sseqp1  34419  poimirlem4  37674  mbfresfi  37716  mbfposadd  37717  itg2gt0cn  37725  sdclem2  37792  mzpcompact2lem  42858  eldiophb  42864  eldioph2  42869  cncfiooicclem1  46005  fouriersw  46343  sge0tsms  46492  psmeasure  46583  sssmf  46850  lindslinindimp2lem2  48574