Theorem fssres 5566

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 5410	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fnssres 5512	. . . . 5 |- ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )
3		resss 5122	. . . . . . 7 |- ( F |` C ) C_ F
4		rnss 5055	. . . . . . 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 3352	. . . . . 6 |- ( ( ran ( F |` C ) C_ ran F /\ ran F C_ B ) -> ran ( F |` C ) C_ B )
7	5, 6	mpan 663	. . . . 5 |- ( ran F C_ B -> ran ( F |` C ) C_ B )
8	2, 7	anim12i 561	. . . 4 |- ( ( ( F Fn A /\ C C_ A ) /\ ran F C_ B ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
9	8	an32s 795	. . 3 |- ( ( ( F Fn A /\ ran F C_ B ) /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
10	1, 9	sylanb 469	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )
11		df-f 5410	. 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 3316   ran crn 4828   |` cres 4829   Fn wfn 5401   -->wf 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-fun 5408  df-fn 5409  df-f 5410

This theorem is referenced by:  fssres2  5567  fresin  5568  fresaun  5570  f1ssres  5601  feqresmpt  5733  f2ndf  6667  elmapssres  7225  pmresg  7228  ralxpmap  7250  mapunen  7468  fofinf1o  7580  fsuppcor  7641  fseqenlem1  8182  inar1  8929  gruima  8956  addnqf  9104  mulnqf  9105  fseq1p1m1  11517  injresinj  11622  seqf1olem2  11829  rlimres  13019  lo1res  13020  vdwnnlem1  14038  ramub2  14057  ramub1lem2  14070  fsets  14182  funcres  14788  resmhm  15468  resghm  15742  gasubg  15799  gsumzres  16367  gsumzresOLD  16371  gsumzaddlem  16387  gsumzadd  16388  gsumzaddlemOLD  16389  gsumzaddOLD  16390  gsum2dlem2  16435  gsum2dOLD  16437  dprdfadd  16483  dprdfaddOLD  16490  dprdres  16498  dprdf1  16503  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dmdprdsplit2lem  16517  dmdprdsplit2  16518  dprdsplit  16520  dpjidcl  16530  dpjidclOLD  16537  ablfac1eulem  16546  ablfac1eu  16547  abvres  16847  pwssplit0  17060  znf1o  17825  frlmsplit2  18038  islindf4  18108  mamures  18131  mdetrlin  18250  cnpresti  18733  cnprest  18734  kgencn  18970  ptrescn  19053  hmeores  19185  ptuncnv  19221  ptunhmeo  19222  ptcmpfi  19227  tsmslem1  19540  tsmssubm  19557  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  tsmsmhm  19561  tsmsadd  19562  tsmsxplem1  19568  tsmsxplem2  19569  psmetres2  19731  xmetres2  19777  metres2  19779  imasdsf1olem  19789  xmetresbl  19853  xrge0gsumle  20251  xrge0tsms  20252  rescncf  20314  ovolicc2lem4  20844  mbfres2  20964  limcdif  21192  limcflf  21197  limcmo  21198  limcres  21202  limciun  21210  dvres  21227  dvres3  21229  dvres3a  21230  dvlip  21306  dvlipcn  21307  dvlip2  21308  dvgt0lem1  21315  dvivthlem1  21321  lhop  21329  aannenlem1  21678  ulmres  21737  ulmss  21746  pserdvlem2  21777  logcn  21976  dvlog  21980  dvlog2  21982  logtayl  21989  dvatan  22214  atancn  22215  efrlim  22247  jensenlem2  22265  jensen  22266  amgm  22268  dchrelbas2  22460  uhgrares  23064  umgrares  23080  redwlk  23327  eupares  23418  issubgoi  23619  hhssnv  24487  resf1o  25854  gsumle  26097  xrge0tsmsd  26105  measres  26489  cntmeas  26493  eulerpartlemt  26601  eulerpartlemmf  26605  eulerpartlemgvv  26606  subiwrd  26615  sseqp1  26625  wrdres  26785  cvmliftlem6  27026  cvmlift2lem11  27049  mbfresfi  28279  mbfposadd  28280  itg2gt0cn  28288  sdclem2  28479  mzpcompact2lem  28930  eldiophb  28937  eldioph2  28942  aomclem4  29252  lincdifsn  30664  lindslinindimp2lem2  30699