MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssres Structured version   Unicode version

Theorem fssres 5763
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
StepHypRef Expression
1 df-f 5602 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
2 fnssres 5704 . . . . 5  |-  ( ( F  Fn  A  /\  C  C_  A )  -> 
( F  |`  C )  Fn  C )
3 resss 5144 . . . . . . 7  |-  ( F  |`  C )  C_  F
4 rnss 5079 . . . . . . 7  |-  ( ( F  |`  C )  C_  F  ->  ran  ( F  |`  C )  C_  ran  F )
53, 4ax-mp 5 . . . . . 6  |-  ran  ( F  |`  C )  C_  ran  F
6 sstr 3472 . . . . . 6  |-  ( ( ran  ( F  |`  C )  C_  ran  F  /\  ran  F  C_  B )  ->  ran  ( F  |`  C ) 
C_  B )
75, 6mpan 674 . . . . 5  |-  ( ran 
F  C_  B  ->  ran  ( F  |`  C ) 
C_  B )
82, 7anim12i 568 . . . 4  |-  ( ( ( F  Fn  A  /\  C  C_  A )  /\  ran  F  C_  B )  ->  (
( F  |`  C )  Fn  C  /\  ran  ( F  |`  C ) 
C_  B ) )
98an32s 811 . . 3  |-  ( ( ( F  Fn  A  /\  ran  F  C_  B
)  /\  C  C_  A
)  ->  ( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B ) )
101, 9sylanb 474 . 2  |-  ( ( F : A --> B  /\  C  C_  A )  -> 
( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B
) )
11 df-f 5602 . 2  |-  ( ( F  |`  C ) : C --> B  <->  ( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B ) )
1210, 11sylibr 215 1  |-  ( ( F : A --> B  /\  C  C_  A )  -> 
( F  |`  C ) : C --> B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3436   ran crn 4851    |` cres 4852    Fn wfn 5593   -->wf 5594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-fun 5600  df-fn 5601  df-f 5602
This theorem is referenced by:  fssresd  5764  fssres2  5765  fresin  5766  fresaun  5768  f1ssres  5800  f2ndf  6910  elmapssres  7501  pmresg  7504  ralxpmap  7526  mapunen  7744  fofinf1o  7855  fseqenlem1  8456  inar1  9201  gruima  9228  addnqf  9374  mulnqf  9375  fseq1p1m1  11869  injresinj  12025  seqf1olem2  12253  rlimres  13610  lo1res  13611  vdwnnlem1  14933  fsets  15137  resmhm  16594  resghm  16887  gsumzres  17531  gsumzadd  17543  gsum2dlem2  17591  dpjidcl  17679  ablfac1eu  17694  abvres  18055  znf1o  19109  islindf4  19383  kgencn  20558  ptrescn  20641  hmeores  20773  tsmsres  21145  tsmsmhm  21147  tsmsadd  21148  xrge0gsumle  21838  xrge0tsms  21839  ovolicc2lem4OLD  22460  ovolicc2lem4  22461  limcdif  22818  limcflf  22823  limcmo  22824  dvres  22853  dvres3a  22856  aannenlem1  23271  logcn  23579  dvlog  23583  dvlog2  23585  logtayl  23592  dvatan  23848  atancn  23849  efrlim  23882  amgm  23903  dchrelbas2  24152  redwlk  25322  issubgoi  26024  hhssnv  26901  xrge0tsmsd  28544  cntmeas  29044  eulerpartlemt  29200  eulerpartlemmf  29204  eulerpartlemgvv  29205  subiwrd  29214  sseqp1  29224  wrdres  29422  poimirlem4  31858  mbfresfi  31901  mbfposadd  31902  itg2gt0cn  31911  sdclem2  31985  mzpcompact2lem  35512  eldiophb  35518  eldioph2  35523  cncfiooicclem1  37591  fouriersw  37915  sge0tsms  38010  psmeasure  38088  resmgmhm  39070  lindslinindimp2lem2  39526
  Copyright terms: Public domain W3C validator