Theorem fssres 5771

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
fssres	|- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )

Proof of Theorem fssres

Step	Hyp	Ref	Expression
1		df-f 5604	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 5710	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5146	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5081	. . . . . . 7 |- ( ( F |` C ) C_ F -> ran ( F |` C ) C_ ran F )
5	3, 4	ax-mp 5	. . . . . 6 |- ran ( F |` C ) C_ ran F
6		sstr 3451	. . . . . 6 |- ( ( ran ( F |` C ) C_ ran F /\ ran F C_ B ) -> ran ( F |` C ) C_ B )
7	5, 6	mpan 681	. . . . 5 |- ( ran F C_ B -> ran ( F |` C ) C_ B )
8	2, 7	anim12i 574	. . . 4 |- ( ( ( F Fn A /\ C C_ A ) /\ ran F C_ B ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
9	8	an32s 818	. . 3 |- ( ( ( F Fn A /\ ran F C_ B ) /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
10	1, 9	sylanb 479	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
11		df-f 5604	. 2 |- ( ( F |` C ) : C --> B <-> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
12	10, 11	sylibr 217	1 |- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )

Syntax hints:   -> wi 4   /\ wa 375   C_ wss 3415   ran crn 4853   |` cres 4854   Fn wfn 5595   -->wf 5596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-fun 5602  df-fn 5603  df-f 5604

This theorem is referenced by:  fssresd  5772  fssres2  5773  fresin  5774  fresaun  5776  f1ssres  5808  f2ndf  6928  elmapssres  7521  pmresg  7524  ralxpmap  7546  mapunen  7766  fofinf1o  7877  fseqenlem1  8480  inar1  9225  gruima  9252  addnqf  9398  mulnqf  9399  fseq1p1m1  11896  injresinj  12056  seqf1olem2  12284  rlimres  13670  lo1res  13671  vdwnnlem1  14993  fsets  15197  resmhm  16654  resghm  16947  gsumzres  17591  gsumzadd  17603  gsum2dlem2  17651  dpjidcl  17739  ablfac1eu  17754  abvres  18115  znf1o  19170  islindf4  19444  kgencn  20619  ptrescn  20702  hmeores  20834  tsmsres  21206  tsmsmhm  21208  tsmsadd  21209  xrge0gsumle  21899  xrge0tsms  21900  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  limcdif  22879  limcflf  22884  limcmo  22885  dvres  22914  dvres3a  22917  aannenlem1  23332  logcn  23640  dvlog  23644  dvlog2  23646  logtayl  23653  dvatan  23909  atancn  23910  efrlim  23943  amgm  23964  dchrelbas2  24213  redwlk  25384  issubgoi  26086  hhssnv  26963  xrge0tsmsd  28596  cntmeas  29096  eulerpartlemt  29252  eulerpartlemmf  29256  eulerpartlemgvv  29257  subiwrd  29266  sseqp1  29276  wrdres  29474  poimirlem4  31988  mbfresfi  32031  mbfposadd  32032  itg2gt0cn  32041  sdclem2  32115  mzpcompact2lem  35637  eldiophb  35643  eldioph2  35648  cncfiooicclem1  37808  fouriersw  38132  sge0tsms  38259  psmeasure  38346  wrdred1  38957  red1wlklem  39715  pthdivtx  39761  resmgmhm  40070  lindslinindimp2lem2  40524