Theorem fssres 5599

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 5443	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 5545	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5155	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5089	. . . . . . 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 3385	. . . . . 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 5443	. 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 3349   ran crn 4862   |` cres 4863   Fn wfn 5434   -->wf 5435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-fun 5441  df-fn 5442  df-f 5443

This theorem is referenced by:  fssres2  5600  fresin  5601  fresaun  5603  f1ssres  5634  feqresmpt  5766  f2ndf  6699  elmapssres  7258  pmresg  7261  ralxpmap  7283  mapunen  7501  fofinf1o  7613  fsuppcor  7674  fseqenlem1  8215  inar1  8963  gruima  8990  addnqf  9138  mulnqf  9139  fseq1p1m1  11555  injresinj  11660  seqf1olem2  11867  rlimres  13057  lo1res  13058  vdwnnlem1  14077  ramub2  14096  ramub1lem2  14109  fsets  14221  funcres  14827  resmhm  15508  resghm  15784  gasubg  15841  gsumzres  16409  gsumzresOLD  16413  gsumzaddlem  16429  gsumzadd  16430  gsumzaddlemOLD  16431  gsumzaddOLD  16432  gsum2dlem2  16484  gsum2dOLD  16486  dprdfadd  16532  dprdfaddOLD  16539  dprdres  16547  dprdf1  16552  dmdprdsplitlem  16556  dmdprdsplitlemOLD  16557  dmdprdsplit2lem  16566  dmdprdsplit2  16567  dprdsplit  16569  dpjidcl  16579  dpjidclOLD  16586  ablfac1eulem  16595  ablfac1eu  16596  abvres  16946  pwssplit0  17161  znf1o  18006  frlmsplit2  18219  islindf4  18289  mamures  18312  mdetrlin  18431  cnpresti  18914  cnprest  18915  kgencn  19151  ptrescn  19234  hmeores  19366  ptuncnv  19402  ptunhmeo  19403  ptcmpfi  19408  tsmslem1  19721  tsmssubm  19738  tsmsresOLD  19739  tsmsres  19740  tsmsf1o  19741  tsmsmhm  19742  tsmsadd  19743  tsmsxplem1  19749  tsmsxplem2  19750  psmetres2  19912  xmetres2  19958  metres2  19960  imasdsf1olem  19970  xmetresbl  20034  xrge0gsumle  20432  xrge0tsms  20433  rescncf  20495  ovolicc2lem4  21025  mbfres2  21145  limcdif  21373  limcflf  21378  limcmo  21379  limcres  21383  limciun  21391  dvres  21408  dvres3  21410  dvres3a  21411  dvlip  21487  dvlipcn  21488  dvlip2  21489  dvgt0lem1  21496  dvivthlem1  21502  lhop  21510  aannenlem1  21816  ulmres  21875  ulmss  21884  pserdvlem2  21915  logcn  22114  dvlog  22118  dvlog2  22120  logtayl  22127  dvatan  22352  atancn  22353  efrlim  22385  jensenlem2  22403  jensen  22404  amgm  22406  dchrelbas2  22598  uhgrares  23264  umgrares  23280  redwlk  23527  eupares  23618  issubgoi  23819  hhssnv  24687  resf1o  26052  gsumle  26268  xrge0tsmsd  26275  measres  26658  cntmeas  26662  eulerpartlemt  26776  eulerpartlemmf  26780  eulerpartlemgvv  26781  subiwrd  26790  sseqp1  26800  wrdres  26960  cvmliftlem6  27201  cvmlift2lem11  27224  mbfresfi  28464  mbfposadd  28465  itg2gt0cn  28473  sdclem2  28664  mzpcompact2lem  29114  eldiophb  29121  eldioph2  29126  aomclem4  29436  lincdifsn  30955  lindslinindimp2lem2  30990