Theorem fssres 5741

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 5582	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 5684	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5287	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5221	. . . . . . 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 3497	. . . . . 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 804	. . 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 5582	. 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 3461   ran crn 4990   |` cres 4991   Fn wfn 5573   -->wf 5574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-fun 5580  df-fn 5581  df-f 5582

This theorem is referenced by:  fssresd  5742  fssres2  5743  fresin  5744  fresaun  5746  f1ssres  5778  f2ndf  6891  elmapssres  7445  pmresg  7448  ralxpmap  7470  mapunen  7688  fofinf1o  7803  fseqenlem1  8408  inar1  9156  gruima  9183  addnqf  9329  mulnqf  9330  fseq1p1m1  11763  injresinj  11908  seqf1olem2  12129  rlimres  13363  lo1res  13364  vdwnnlem1  14495  fsets  14640  resmhm  15969  resghm  16262  gsumzres  16893  gsumzresOLD  16897  gsumzadd  16914  gsumzaddlemOLD  16915  gsumzaddOLD  16916  gsum2dlem2  16977  gsum2dOLD  16979  dprdfaddOLD  17046  dmdprdsplitlemOLD  17064  dpjidcl  17086  dpjidclOLD  17093  ablfac1eu  17103  abvres  17467  znf1o  18568  islindf4  18851  kgencn  20035  ptrescn  20118  hmeores  20250  tsmsresOLD  20623  tsmsres  20624  tsmsmhm  20626  tsmsadd  20627  xrge0gsumle  21316  xrge0tsms  21317  ovolicc2lem4  21909  limcdif  22258  limcflf  22263  limcmo  22264  dvres  22293  dvres3a  22296  aannenlem1  22702  logcn  23006  dvlog  23010  dvlog2  23012  logtayl  23019  dvatan  23244  atancn  23245  efrlim  23277  amgm  23298  dchrelbas2  23490  redwlk  24586  issubgoi  25290  hhssnv  26158  xrge0tsmsd  27753  cntmeas  28175  eulerpartlemt  28288  eulerpartlemmf  28292  eulerpartlemgvv  28293  subiwrd  28302  sseqp1  28312  wrdres  28472  mbfresfi  30037  mbfposadd  30038  itg2gt0cn  30046  sdclem2  30211  mzpcompact2lem  30660  eldiophb  30666  eldioph2  30671  cncfiooicclem1  31650  fouriersw  31968  resmgmhm  32440  lindslinindimp2lem2  32930