Theorem fssres 6708

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 6504	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6623	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5968	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5897	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3944	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 691	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 614	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 653	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6504	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903  ran crn 5633   ↾ cres 5634   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fssresd  6709  fssres2  6710  fresin  6711  fresaun  6713  f1ssres  6745  resf1extb  7886  resf1ext2b  7887  f2ndf  8072  elmapssres  8816  pmresg  8820  ralxpmap  8846  mapunen  9086  fofinf1o  9244  fseqenlem1  9946  inar1  10698  gruima  10725  addnqf  10871  mulnqf  10872  fseq1p1m1  13526  injresinj  13719  seqf1olem2  13977  wrdred1  14495  rlimres  15493  lo1res  15494  vdwnnlem1  16935  fsets  17108  resmgmhm  18648  resmhm  18757  resghm  19173  gsumzres  19850  gsumzadd  19863  gsum2dlem2  19912  dpjidcl  20001  ablfac1eu  20016  abvres  20776  znf1o  21518  islindf4  21805  kgencn  23512  ptrescn  23595  hmeores  23727  tsmsres  24100  tsmsmhm  24102  tsmsadd  24103  xrge0gsumle  24790  xrge0tsms  24791  ovolicc2lem4  25489  limcdif  25845  limcflf  25850  limcmo  25851  dvres  25880  dvres3a  25883  aannenlem1  26304  logcn  26624  dvlog  26628  dvlog2  26630  logtayl  26637  dvatan  26913  atancn  26914  efrlim  26947  efrlimOLD  26948  amgm  26969  dchrelbas2  27216  redwlklem  29755  pthdivtx  29812  hhssabloilem  31348  hhssnv  31351  wrdres  33027  gsumpart  33156  xrge0tsmsd  33166  cntmeas  34403  eulerpartlemt  34548  eulerpartlemmf  34552  eulerpartlemgvv  34553  subiwrd  34562  sseqp1  34572  poimirlem4  37872  mbfresfi  37914  mbfposadd  37915  itg2gt0cn  37923  sdclem2  37990  mzpcompact2lem  43105  eldiophb  43111  eldioph2  43116  cncfiooicclem1  46248  fouriersw  46586  sge0tsms  46735  psmeasure  46826  sssmf  47093  lindslinindimp2lem2  48816