Theorem fssres 6543

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 6358	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6469	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5877	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5809	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3974	. . . . . 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 6358	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 236	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3935  ran crn 5555   ↾ cres 5556   Fn wfn 6349  ⟶wf 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-opab 5128  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-fun 6356  df-fn 6357  df-f 6358

This theorem is referenced by:  fssresd  6544  fssres2  6545  fresin  6546  fresaun  6548  f1ssres  6581  f2ndf  7815  elmapssres  8430  pmresg  8433  ralxpmap  8459  mapunen  8685  fofinf1o  8798  fseqenlem1  9449  inar1  10196  gruima  10223  addnqf  10369  mulnqf  10370  fseq1p1m1  12980  injresinj  13157  seqf1olem2  13409  wrdred1  13911  rlimres  14914  lo1res  14915  vdwnnlem1  16330  fsets  16515  resmhm  17984  resghm  18373  gsumzres  19028  gsumzadd  19041  gsum2dlem2  19090  dpjidcl  19179  ablfac1eu  19194  abvres  19609  znf1o  20697  islindf4  20981  kgencn  22163  ptrescn  22246  hmeores  22378  tsmsres  22751  tsmsmhm  22753  tsmsadd  22754  xrge0gsumle  23440  xrge0tsms  23441  ovolicc2lem4  24120  limcdif  24473  limcflf  24478  limcmo  24479  dvres  24508  dvres3a  24511  aannenlem1  24916  logcn  25229  dvlog  25233  dvlog2  25235  logtayl  25242  dvatan  25512  atancn  25513  efrlim  25546  amgm  25567  dchrelbas2  25812  redwlklem  27452  pthdivtx  27509  hhssabloilem  29037  hhssnv  29040  wrdres  30613  xrge0tsmsd  30692  cntmeas  31485  eulerpartlemt  31629  eulerpartlemmf  31633  eulerpartlemgvv  31634  subiwrd  31643  sseqp1  31653  poimirlem4  34895  mbfresfi  34937  mbfposadd  34938  itg2gt0cn  34946  sdclem2  35016  mzpcompact2lem  39346  eldiophb  39352  eldioph2  39357  cncfiooicclem1  42174  fouriersw  42515  sge0tsms  42661  psmeasure  42752  sssmf  43014  resmgmhm  44064  lindslinindimp2lem2  44513