Theorem fssres 6747

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 6539	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6663	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6001	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5934	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3988	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 689	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 614	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 651	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6539	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 233	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3946  ran crn 5673   ↾ cres 5674   Fn wfn 6530  ⟶wf 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5295  ax-nul 5302  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5145  df-opab 5207  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-fun 6537  df-fn 6538  df-f 6539

This theorem is referenced by:  fssresd  6748  fssres2  6749  fresin  6750  fresaun  6752  f1ssres  6785  f2ndf  8093  elmapssres  8849  pmresg  8852  ralxpmap  8878  mapunen  9134  fofinf1o  9315  fseqenlem1  10006  inar1  10757  gruima  10784  addnqf  10930  mulnqf  10931  fseq1p1m1  13562  injresinj  13740  seqf1olem2  13995  wrdred1  14497  rlimres  15489  lo1res  15490  vdwnnlem1  16915  fsets  17089  resmhm  18688  resghm  19093  gsumzres  19760  gsumzadd  19773  gsum2dlem2  19822  dpjidcl  19911  ablfac1eu  19926  abvres  20424  znf1o  21080  islindf4  21366  kgencn  23029  ptrescn  23112  hmeores  23244  tsmsres  23617  tsmsmhm  23619  tsmsadd  23620  xrge0gsumle  24318  xrge0tsms  24319  ovolicc2lem4  25006  limcdif  25362  limcflf  25367  limcmo  25368  dvres  25397  dvres3a  25400  aannenlem1  25810  logcn  26124  dvlog  26128  dvlog2  26130  logtayl  26137  dvatan  26407  atancn  26408  efrlim  26441  amgm  26462  dchrelbas2  26707  redwlklem  28895  pthdivtx  28953  hhssabloilem  30479  hhssnv  30482  wrdres  32074  gsumpart  32178  xrge0tsmsd  32180  cntmeas  33155  eulerpartlemt  33301  eulerpartlemmf  33305  eulerpartlemgvv  33306  subiwrd  33315  sseqp1  33325  poimirlem4  36397  mbfresfi  36439  mbfposadd  36440  itg2gt0cn  36448  sdclem2  36516  mzpcompact2lem  41360  eldiophb  41366  eldioph2  41371  cncfiooicclem1  44482  fouriersw  44820  sge0tsms  44969  psmeasure  45060  sssmf  45327  resmgmhm  46441  lindslinindimp2lem2  46980