Theorem fssres 6322

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 6141	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6252	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5673	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5602	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3829	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 680	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 606	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 642	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 576	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6141	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 226	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 386   ⊆ wss 3792  ran crn 5358   ↾ cres 5359   Fn wfn 6132  ⟶wf 6133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889  df-opab 4951  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-fun 6139  df-fn 6140  df-f 6141

This theorem is referenced by:  fssresd  6323  fssres2  6324  fresin  6325  fresaun  6327  f1ssres  6360  f2ndf  7566  elmapssres  8167  pmresg  8170  ralxpmap  8195  mapunen  8419  fofinf1o  8531  fseqenlem1  9182  inar1  9934  gruima  9961  addnqf  10107  mulnqf  10108  fseq1p1m1  12737  injresinj  12913  seqf1olem2  13164  wrdred1  13656  rlimres  14706  lo1res  14707  vdwnnlem1  16114  fsets  16299  resmhm  17756  resghm  18071  gsumzres  18707  gsumzadd  18719  gsum2dlem2  18767  dpjidcl  18855  ablfac1eu  18870  abvres  19242  znf1o  20306  islindf4  20592  kgencn  21779  ptrescn  21862  hmeores  21994  tsmsres  22366  tsmsmhm  22368  tsmsadd  22369  xrge0gsumle  23055  xrge0tsms  23056  ovolicc2lem4  23735  limcdif  24088  limcflf  24093  limcmo  24094  dvres  24123  dvres3a  24126  aannenlem1  24531  logcn  24841  dvlog  24845  dvlog2  24847  logtayl  24854  dvatan  25124  atancn  25125  efrlim  25159  amgm  25180  dchrelbas2  25425  redwlklem  27039  pthdivtx  27098  hhssabloilem  28707  hhssnv  28710  xrge0tsmsd  30355  cntmeas  30895  eulerpartlemt  31039  eulerpartlemmf  31043  eulerpartlemgvv  31044  subiwrd  31053  sseqp1  31064  wrdres  31224  poimirlem4  34048  mbfresfi  34090  mbfposadd  34091  itg2gt0cn  34099  sdclem2  34171  mzpcompact2lem  38288  eldiophb  38294  eldioph2  38299  cncfiooicclem1  41048  fouriersw  41389  sge0tsms  41535  psmeasure  41626  sssmf  41888  resmgmhm  42827  lindslinindimp2lem2  43277