Theorem fssres 6070

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 5892	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 6004	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5422	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5354	. . . . . . 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 3611	. . . . . 6 |- ( ( ran ( F |` C ) C_ ran F /\ ran F C_ B ) -> ran ( F |` C ) C_ B )
7	5, 6	mpan 706	. . . . 5 |- ( ran F C_ B -> ran ( F |` C ) C_ B )
8	2, 7	anim12i 590	. . . 4 |- ( ( ( F Fn A /\ C C_ A ) /\ ran F C_ B ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
9	8	an32s 846	. . 3 |- ( ( ( F Fn A /\ ran F C_ B ) /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
10	1, 9	sylanb 489	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
11		df-f 5892	. 2 |- ( ( F |` C ) : C --> B <-> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
12	10, 11	sylibr 224	1 |- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )

Syntax hints:   -> wi 4   /\ wa 384   C_ wss 3574   ran crn 5115   |` cres 5116   Fn wfn 5883   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  fssresd  6071  fssres2  6072  fresin  6073  fresaun  6075  f1ssres  6108  f2ndf  7283  elmapssres  7882  pmresg  7885  ralxpmap  7907  mapunen  8129  fofinf1o  8241  fseqenlem1  8847  inar1  9597  gruima  9624  addnqf  9770  mulnqf  9771  fseq1p1m1  12414  injresinj  12589  seqf1olem2  12841  wrdred1  13349  rlimres  14289  lo1res  14290  vdwnnlem1  15699  fsets  15891  resmhm  17359  resghm  17676  gsumzres  18310  gsumzadd  18322  gsum2dlem2  18370  dpjidcl  18457  ablfac1eu  18472  abvres  18839  znf1o  19900  islindf4  20177  kgencn  21359  ptrescn  21442  hmeores  21574  tsmsres  21947  tsmsmhm  21949  tsmsadd  21950  xrge0gsumle  22636  xrge0tsms  22637  ovolicc2lem4  23288  limcdif  23640  limcflf  23645  limcmo  23646  dvres  23675  dvres3a  23678  aannenlem1  24083  logcn  24393  dvlog  24397  dvlog2  24399  logtayl  24406  dvatan  24662  atancn  24663  efrlim  24696  amgm  24717  dchrelbas2  24962  redwlklem  26568  pthdivtx  26625  hhssabloilem  28118  hhssnv  28121  xrge0tsmsd  29785  cntmeas  30289  eulerpartlemt  30433  eulerpartlemmf  30437  eulerpartlemgvv  30438  subiwrd  30447  sseqp1  30457  wrdres  30617  poimirlem4  33413  mbfresfi  33456  mbfposadd  33457  itg2gt0cn  33465  sdclem2  33538  mzpcompact2lem  37314  eldiophb  37320  eldioph2  37325  cncfiooicclem1  40106  fouriersw  40448  sge0tsms  40597  psmeasure  40688  sssmf  40947  resmgmhm  41798  lindslinindimp2lem2  42248