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

Theorem fores 5498
Description: Restriction of a function. (Contributed by NM, 4-Mar-1997.)
Assertion
Ref Expression
fores  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( F  |`  A ) : A -onto-> ( F
" A ) )

Proof of Theorem fores
StepHypRef Expression
1 funres 5330 . . 3  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )
21anim1i 551 . 2  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( Fun  ( F  |`  A )  /\  A  C_ 
dom  F ) )
3 df-fn 5295 . . 3  |-  ( ( F  |`  A )  Fn  A  <->  ( Fun  ( F  |`  A )  /\  dom  ( F  |`  A )  =  A ) )
4 df-ima 4739 . . . . 5  |-  ( F
" A )  =  ran  ( F  |`  A )
54eqcomi 2320 . . . 4  |-  ran  ( F  |`  A )  =  ( F " A
)
6 df-fo 5298 . . . 4  |-  ( ( F  |`  A ) : A -onto-> ( F " A )  <->  ( ( F  |`  A )  Fn  A  /\  ran  ( F  |`  A )  =  ( F " A
) ) )
75, 6mpbiran2 885 . . 3  |-  ( ( F  |`  A ) : A -onto-> ( F " A )  <->  ( F  |`  A )  Fn  A
)
8 ssdmres 5014 . . . 4  |-  ( A 
C_  dom  F  <->  dom  ( F  |`  A )  =  A )
98anbi2i 675 . . 3  |-  ( ( Fun  ( F  |`  A )  /\  A  C_ 
dom  F )  <->  ( Fun  ( F  |`  A )  /\  dom  ( F  |`  A )  =  A ) )
103, 7, 93bitr4i 268 . 2  |-  ( ( F  |`  A ) : A -onto-> ( F " A )  <->  ( Fun  ( F  |`  A )  /\  A  C_  dom  F ) )
112, 10sylibr 203 1  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( F  |`  A ) : A -onto-> ( F
" A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1633    C_ wss 3186   dom cdm 4726   ran crn 4727    |` cres 4728   "cima 4729   Fun wfun 5286    Fn wfn 5287   -onto->wfo 5290
This theorem is referenced by:  resdif  5532  f1oweALT  5893  imafi  7193  f1opwfi  7204  fodomfi2  7732  fin1a2lem7  8077  znnen  12538  conima  17207  1stcfb  17227  1stckgenlem  17304  qtoprest  17464  re2ndc  18359  uniiccdif  18986  opnmblALT  19011  mbfimaopnlem  19063  ghsubgolem  21090  erdszelem2  24007  ivthALT  25407  lmhmfgima  26330
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-res 4738  df-ima 4739  df-fun 5294  df-fn 5295  df-fo 5298
  Copyright terms: Public domain W3C validator