Theorem fssres 6706

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 6502	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6621	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5966	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5895	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3930	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 691	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 614	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 653	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6502	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3889  ran crn 5632   ↾ cres 5633   Fn wfn 6493  ⟶wf 6494

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  fssresd  6707  fssres2  6708  fresin  6709  fresaun  6711  f1ssres  6743  resf1extb  7885  resf1ext2b  7886  f2ndf  8070  elmapssres  8814  pmresg  8818  ralxpmap  8844  mapunen  9084  fofinf1o  9242  fseqenlem1  9946  inar1  10698  gruima  10725  addnqf  10871  mulnqf  10872  fseq1p1m1  13552  injresinj  13746  seqf1olem2  14004  wrdred1  14522  rlimres  15520  lo1res  15521  vdwnnlem1  16966  fsets  17139  resmgmhm  18679  resmhm  18788  resghm  19207  gsumzres  19884  gsumzadd  19897  gsum2dlem2  19946  dpjidcl  20035  ablfac1eu  20050  abvres  20808  znf1o  21531  islindf4  21818  kgencn  23521  ptrescn  23604  hmeores  23736  tsmsres  24109  tsmsmhm  24111  tsmsadd  24112  xrge0gsumle  24799  xrge0tsms  24800  ovolicc2lem4  25487  limcdif  25843  limcflf  25848  limcmo  25849  dvres  25878  dvres3a  25881  aannenlem1  26294  logcn  26611  dvlog  26615  dvlog2  26617  logtayl  26624  dvatan  26899  atancn  26900  efrlim  26933  amgm  26954  dchrelbas2  27200  redwlklem  29738  pthdivtx  29795  hhssabloilem  31332  hhssnv  31335  wrdres  32995  gsumpart  33124  xrge0tsmsd  33134  cntmeas  34370  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpartlemgvv  34520  subiwrd  34529  sseqp1  34539  poimirlem4  37945  mbfresfi  37987  mbfposadd  37988  itg2gt0cn  37996  sdclem2  38063  mzpcompact2lem  43183  eldiophb  43189  eldioph2  43194  cncfiooicclem1  46321  fouriersw  46659  sge0tsms  46808  psmeasure  46899  sssmf  47166  lindslinindimp2lem2  48935