Theorem fssres 6743

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 6534	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6660	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5988	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5920	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3967	. . . . . 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 6534	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926  ran crn 5655   ↾ cres 5656   Fn wfn 6525  ⟶wf 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  fssresd  6744  fssres2  6745  fresin  6746  fresaun  6748  f1ssres  6780  resf1extb  7928  resf1ext2b  7929  f2ndf  8117  elmapssres  8879  pmresg  8882  ralxpmap  8908  mapunen  9158  fofinf1o  9342  fseqenlem1  10036  inar1  10787  gruima  10814  addnqf  10960  mulnqf  10961  fseq1p1m1  13613  injresinj  13802  seqf1olem2  14058  wrdred1  14576  rlimres  15572  lo1res  15573  vdwnnlem1  17013  fsets  17186  resmgmhm  18687  resmhm  18796  resghm  19213  gsumzres  19888  gsumzadd  19901  gsum2dlem2  19950  dpjidcl  20039  ablfac1eu  20054  abvres  20789  znf1o  21510  islindf4  21796  kgencn  23492  ptrescn  23575  hmeores  23707  tsmsres  24080  tsmsmhm  24082  tsmsadd  24083  xrge0gsumle  24771  xrge0tsms  24772  ovolicc2lem4  25471  limcdif  25827  limcflf  25832  limcmo  25833  dvres  25862  dvres3a  25865  aannenlem1  26286  logcn  26606  dvlog  26610  dvlog2  26612  logtayl  26619  dvatan  26895  atancn  26896  efrlim  26929  efrlimOLD  26930  amgm  26951  dchrelbas2  27198  redwlklem  29597  pthdivtx  29655  hhssabloilem  31188  hhssnv  31191  wrdres  32856  gsumpart  32997  xrge0tsmsd  33002  cntmeas  34203  eulerpartlemt  34349  eulerpartlemmf  34353  eulerpartlemgvv  34354  subiwrd  34363  sseqp1  34373  poimirlem4  37594  mbfresfi  37636  mbfposadd  37637  itg2gt0cn  37645  sdclem2  37712  mzpcompact2lem  42721  eldiophb  42727  eldioph2  42732  cncfiooicclem1  45870  fouriersw  46208  sge0tsms  46357  psmeasure  46448  sssmf  46715  lindslinindimp2lem2  48383