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

Theorem fssres 5408
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 5259 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
2 fnssres 5357 . . . . 5  |-  ( ( F  Fn  A  /\  C  C_  A )  -> 
( F  |`  C )  Fn  C )
3 resss 4979 . . . . . . 7  |-  ( F  |`  C )  C_  F
4 rnss 4907 . . . . . . 7  |-  ( ( F  |`  C )  C_  F  ->  ran  ( F  |`  C )  C_  ran  F )
53, 4ax-mp 8 . . . . . 6  |-  ran  ( F  |`  C )  C_  ran  F
6 sstr 3187 . . . . . 6  |-  ( ( ran  ( F  |`  C )  C_  ran  F  /\  ran  F  C_  B )  ->  ran  ( F  |`  C ) 
C_  B )
75, 6mpan 651 . . . . 5  |-  ( ran 
F  C_  B  ->  ran  ( F  |`  C ) 
C_  B )
82, 7anim12i 549 . . . 4  |-  ( ( ( F  Fn  A  /\  C  C_  A )  /\  ran  F  C_  B )  ->  (
( F  |`  C )  Fn  C  /\  ran  ( F  |`  C ) 
C_  B ) )
98an32s 779 . . 3  |-  ( ( ( F  Fn  A  /\  ran  F  C_  B
)  /\  C  C_  A
)  ->  ( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B ) )
101, 9sylanb 458 . 2  |-  ( ( F : A --> B  /\  C  C_  A )  -> 
( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B
) )
11 df-f 5259 . 2  |-  ( ( F  |`  C ) : C --> B  <->  ( ( F  |`  C )  Fn  C  /\  ran  ( F  |`  C )  C_  B ) )
1210, 11sylibr 203 1  |-  ( ( F : A --> B  /\  C  C_  A )  -> 
( F  |`  C ) : C --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152   ran crn 4690    |` cres 4691    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fssres2  5409  fresin  5410  fresaun  5412  f1ssres  5444  feqresmpt  5576  pmresg  6795  mapunen  7030  fofinf1o  7137  fseqenlem1  7651  inar1  8397  gruima  8424  addnqf  8572  mulnqf  8573  fseq1p1m1  10857  seqf1olem2  11086  rlimres  12032  lo1res  12033  vdwnnlem1  13042  ramub2  13061  ramub1lem2  13074  funcres  13770  resmhm  14436  resghm  14699  gasubg  14756  gsumzres  15194  gsumzaddlem  15203  gsumzadd  15204  gsum2d  15223  dprdfadd  15255  dprdres  15263  dprdf1  15268  dmdprdsplitlem  15272  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dprdsplit  15283  dpjidcl  15293  ablfac1eulem  15307  ablfac1eu  15308  abvres  15604  znf1o  16505  cnpresti  17016  cnprest  17017  kgencn  17251  ptrescn  17333  hmeores  17462  ptuncnv  17498  ptunhmeo  17499  ptcmpfi  17504  tsmslem1  17811  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  tsmsmhm  17828  tsmsadd  17829  tsmsxplem1  17835  tsmsxplem2  17836  xmetres2  17925  metres2  17927  imasdsf1olem  17937  xmetresbl  17983  xrge0gsumle  18338  xrge0tsms  18339  rescncf  18401  ovolicc2lem4  18879  mbfres2  19000  limcdif  19226  limcflf  19231  limcmo  19232  limcres  19236  limciun  19244  dvres  19261  dvres3  19263  dvres3a  19264  dvlip  19340  dvlipcn  19341  dvlip2  19342  dvgt0lem1  19349  dvivthlem1  19355  lhop  19363  aannenlem1  19708  ulmres  19767  ulmss  19774  pserdvlem2  19804  logcn  19994  dvlog  19998  dvlog2  20000  logtayl  20007  dvatan  20231  atancn  20232  efrlim  20264  jensenlem2  20282  jensen  20283  amgm  20285  dchrelbas2  20476  issubgoi  20977  hhssnv  21841  xrge0tsmsd  23382  measres  23549  cntmeas  23553  coinflipspace  23681  cvmliftlem6  23821  cvmlift2lem11  23844  umgrares  23876  eupares  23899  nZdef  25180  islimrs3  25581  islimrs4  25582  sdclem2  26452  ralxpmap  26761  elmapssres  26792  mzpcompact2lem  26829  eldiophb  26836  eldioph2  26841  aomclem4  27154  pwssplit0  27187  frlmsplit2  27243  islindf4  27308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-fun 5257  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator