Theorem fssres 6773

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 6565	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6687	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6004	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5930	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3921	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 703	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 625	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 665	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 593	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6565	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 237	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900  ran crn 5657   ↾ cres 5658   Fn wfn 6556  ⟶wf 6557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  fssresd  6774  fssres2  6775  fresin  6776  fresaun  6778  f1ssres  6812  resf1extb  7973  resf1ext2b  7974  f2ndf  8161  tz7.48lem  8481  elmapssres  8925  pmresg  8929  ralxpmap  8955  mapunen  9196  fofinf1o  9352  fseqenlem1  10133  inar1  10890  gruima  10917  addnqf  11063  mulnqf  11064  fseq1p1m1  13762  injresinj  13956  seqf1olem2  14215  wrdred1  14735  rlimres  15757  lo1res  15758  vdwnnlem1  17205  fsets  17379  resmgmhm  18932  resmhm  19048  resghm  19478  gsumzres  20156  gsumzadd  20169  gsum2dlem2  20218  dpjidcl  20307  ablfac1eu  20322  abvres  21121  znf1o  21890  islindf4  22177  kgencn  23908  ptrescn  23991  hmeores  24123  tsmsres  24496  tsmsmhm  24498  tsmsadd  24499  xrge0gsumle  25186  xrge0tsms  25187  ovolicc2lem4  25874  limcdif  26229  limcflf  26234  limcmo  26235  dvres  26264  dvres3a  26267  aannenlem1  26688  logcn  27008  dvlog  27012  dvlog2  27014  logtayl  27021  dvatan  27296  atancn  27297  efrlim  27330  amgm  27351  dchrelbas2  27597  redwlklem  30283  pthdivtx  30345  hhssabloilem  31896  hhssnv  31899  wrdres  33575  gsumpart  33700  xrge0tsmsd  33710  cntmeas  34942  eulerpartlemt  35086  eulerpartlemmf  35090  eulerpartlemgvv  35091  subiwrd  35100  sseqp1  35110  werankwe  35834  werankwe2  35835  acwer1prc  35865  poimirlem4  38747  mbfresfi  38789  mbfposadd  38790  itg2gt0cn  38798  sdclem2  38879  mzpcompact2lem  43966  eldiophb  43972  eldioph2  43977  cncfiooicclem1  47118  fouriersw  47456  sge0tsms  47605  psmeasure  47696  lindslinindimp2lem2  49786