Theorem fssres 6546

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 6361	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6472	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5880	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5812	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3977	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 688	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 614	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 650	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 583	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6361	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 236	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3938  ran crn 5558   ↾ cres 5559   Fn wfn 6352  ⟶wf 6353

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  fssresd  6547  fssres2  6548  fresin  6549  fresaun  6551  f1ssres  6584  f2ndf  7818  elmapssres  8433  pmresg  8436  ralxpmap  8462  mapunen  8688  fofinf1o  8801  fseqenlem1  9452  inar1  10199  gruima  10226  addnqf  10372  mulnqf  10373  fseq1p1m1  12984  injresinj  13161  seqf1olem2  13413  wrdred1  13914  rlimres  14917  lo1res  14918  vdwnnlem1  16333  fsets  16518  resmhm  17987  resghm  18376  gsumzres  19031  gsumzadd  19044  gsum2dlem2  19093  dpjidcl  19182  ablfac1eu  19197  abvres  19612  znf1o  20700  islindf4  20984  kgencn  22166  ptrescn  22249  hmeores  22381  tsmsres  22754  tsmsmhm  22756  tsmsadd  22757  xrge0gsumle  23443  xrge0tsms  23444  ovolicc2lem4  24123  limcdif  24476  limcflf  24481  limcmo  24482  dvres  24511  dvres3a  24514  aannenlem1  24919  logcn  25232  dvlog  25236  dvlog2  25238  logtayl  25245  dvatan  25515  atancn  25516  efrlim  25549  amgm  25570  dchrelbas2  25815  redwlklem  27455  pthdivtx  27512  hhssabloilem  29040  hhssnv  29043  wrdres  30615  xrge0tsmsd  30694  cntmeas  31487  eulerpartlemt  31631  eulerpartlemmf  31635  eulerpartlemgvv  31636  subiwrd  31645  sseqp1  31655  poimirlem4  34898  mbfresfi  34940  mbfposadd  34941  itg2gt0cn  34949  sdclem2  35019  mzpcompact2lem  39355  eldiophb  39361  eldioph2  39366  cncfiooicclem1  42183  fouriersw  42523  sge0tsms  42669  psmeasure  42760  sssmf  43022  resmgmhm  44072  lindslinindimp2lem2  44521