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

Theorem dffo2 5797
Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
Assertion
Ref Expression
dffo2  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )

Proof of Theorem dffo2
StepHypRef Expression
1 fof 5793 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5796 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 532 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5729 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5592 . . . 4  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
65biimpri 206 . . 3  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  F : A -onto-> B )
74, 6sylan 471 . 2  |-  ( ( F : A --> B  /\  ran  F  =  B )  ->  F : A -onto-> B )
83, 7impbii 188 1  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1379   ran crn 5000    Fn wfn 5581   -->wf 5582   -onto->wfo 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5590  df-fo 5592
This theorem is referenced by:  foco  5803  foconst  5804  dff1o5  5823  dffo3  6034  dffo4  6035  exfo  6037  fo1stres  6805  fo2ndres  6806  fo2ndf  6887  cantnf  8108  cantnfOLD  8130  hsmexlem2  8803  1fv  11785  setcepi  15269  odf1o1  16388  efgsfo  16553  pjfo  18513  xrhmeo  21181  fargshiftfo  24314  grpofo  24877  cnpcon  28315  lnmepi  30635
  Copyright terms: Public domain W3C validator