Theorem fssres 5751

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 5592	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 5694	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5297	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5231	. . . . . . 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 3512	. . . . . 6 |- ( ( ran ( F |` C ) C_ ran F /\ ran F C_ B ) -> ran ( F |` C ) C_ B )
7	5, 6	mpan 670	. . . . 5 |- ( ran F C_ B -> ran ( F |` C ) C_ B )
8	2, 7	anim12i 566	. . . 4 |- ( ( ( F Fn A /\ C C_ A ) /\ ran F C_ B ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
9	8	an32s 802	. . 3 |- ( ( ( F Fn A /\ ran F C_ B ) /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
10	1, 9	sylanb 472	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
11		df-f 5592	. 2 |- ( ( F |` C ) : C --> B <-> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
12	10, 11	sylibr 212	1 |- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )

Syntax hints:   -> wi 4   /\ wa 369   C_ wss 3476   ran crn 5000   |` cres 5001   Fn wfn 5583   -->wf 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-fun 5590  df-fn 5591  df-f 5592

This theorem is referenced by:  fssresd  5752  fssres2  5753  fresin  5754  fresaun  5756  f1ssres  5788  feqresmpt  5921  f2ndf  6889  elmapssres  7443  pmresg  7446  ralxpmap  7468  mapunen  7686  fofinf1o  7801  fsuppcor  7863  fseqenlem1  8405  inar1  9153  gruima  9180  addnqf  9326  mulnqf  9327  fseq1p1m1  11752  injresinj  11894  seqf1olem2  12115  rlimres  13344  lo1res  13345  vdwnnlem1  14372  ramub2  14391  ramub1lem2  14404  fsets  14516  funcres  15123  resmhm  15809  resghm  16088  gasubg  16145  gsumzres  16717  gsumzresOLD  16721  gsumzaddlem  16737  gsumzadd  16738  gsumzaddlemOLD  16739  gsumzaddOLD  16740  gsum2dlem2  16801  gsum2dOLD  16803  dprdfadd  16862  dprdfaddOLD  16869  dprdres  16877  dprdf1  16882  dmdprdsplitlem  16886  dmdprdsplitlemOLD  16887  dmdprdsplit2lem  16896  dmdprdsplit2  16897  dprdsplit  16899  dpjidcl  16909  dpjidclOLD  16916  ablfac1eulem  16925  ablfac1eu  16926  abvres  17288  pwssplit0  17504  znf1o  18385  frlmsplit2  18598  islindf4  18668  mamures  18687  mdetrlin  18899  cnpresti  19583  cnprest  19584  kgencn  19820  ptrescn  19903  hmeores  20035  ptuncnv  20071  ptunhmeo  20072  ptcmpfi  20077  tsmslem1  20390  tsmssubm  20407  tsmsresOLD  20408  tsmsres  20409  tsmsf1o  20410  tsmsmhm  20411  tsmsadd  20412  tsmsxplem1  20418  tsmsxplem2  20419  psmetres2  20581  xmetres2  20627  metres2  20629  imasdsf1olem  20639  xmetresbl  20703  xrge0gsumle  21101  xrge0tsms  21102  rescncf  21164  ovolicc2lem4  21694  mbfres2  21815  limcdif  22043  limcflf  22048  limcmo  22049  limcres  22053  limciun  22061  dvres  22078  dvres3  22080  dvres3a  22081  dvlip  22157  dvlipcn  22158  dvlip2  22159  dvgt0lem1  22166  dvivthlem1  22172  lhop  22180  aannenlem1  22486  ulmres  22545  ulmss  22554  pserdvlem2  22585  logcn  22784  dvlog  22788  dvlog2  22790  logtayl  22797  dvatan  23022  atancn  23023  efrlim  23055  jensenlem2  23073  jensen  23074  amgm  23076  dchrelbas2  23268  uhgrares  24012  umgrares  24028  redwlk  24312  eupares  24679  issubgoi  25016  hhssnv  25884  resf1o  27253  gsumle  27461  xrge0tsmsd  27466  measres  27861  cntmeas  27865  eulerpartlemt  27978  eulerpartlemmf  27982  eulerpartlemgvv  27983  subiwrd  27992  sseqp1  28002  wrdres  28162  cvmliftlem6  28403  cvmlift2lem11  28426  mbfresfi  29666  mbfposadd  29667  itg2gt0cn  29675  sdclem2  29866  mzpcompact2lem  30316  eldiophb  30322  eldioph2  30327  aomclem4  30635  limcperiod  31198  cncfperiod  31245  cncfiooicclem1  31260  dirkercncflem4  31434  fourierdlem53  31488  fourierdlem75  31510  fourierdlem88  31523  fourierdlem93  31528  fourierdlem100  31535  fourierdlem111  31546  fourierdlem112  31547  fourierdlem113  31548  fouriersw  31560  lincdifsn  32124  lindslinindimp2lem2  32159