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

Theorem dffo2 5782
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 5778 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5781 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 530 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5714 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5575 . . . 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 469 . 2  |-  ( ( F : A --> B  /\  ran  F  =  B )  ->  F : A -onto-> B )
83, 7impbii 187 1  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    = wceq 1405   ran crn 4824    Fn wfn 5564   -->wf 5565   -onto->wfo 5567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428  df-f 5573  df-fo 5575
This theorem is referenced by:  foco  5788  foconst  5789  dff1o5  5808  dffo3  6024  dffo4  6025  exfo  6027  fo1stres  6808  fo2ndres  6809  fo2ndf  6891  cantnf  8144  cantnfOLD  8166  hsmexlem2  8839  1fv  11847  setcepi  15691  odf1o1  16916  efgsfo  17081  pjfo  19044  xrhmeo  21738  fargshiftfo  25055  grpofo  25615  cnpcon  29527  lnmepi  35393
  Copyright terms: Public domain W3C validator