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

Theorem dffo2 5538
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 5534 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5537 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 518 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5472 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5343 . . . 4  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
65biimpri 197 . . 3  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  F : A -onto-> B )
74, 6sylan 457 . 2  |-  ( ( F : A --> B  /\  ran  F  =  B )  ->  F : A -onto-> B )
83, 7impbii 180 1  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1642   ran crn 4772    Fn wfn 5332   -->wf 5333   -onto->wfo 5335
This theorem is referenced by:  foco  5544  foconst  5545  dff1o5  5564  dffo3  5758  dffo4  5759  exfo  5761  fo1stres  6230  fo2ndres  6231  cantnf  7485  hsmexlem2  8143  setcepi  14019  odf1o1  14982  efgsfo  15147  pjfo  16721  xrhmeo  18548  grpofo  20978  cnpcon  24165  lnmepi  26506  1fv  27456  fargshiftfo  27761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242  df-f 5341  df-fo 5343
  Copyright terms: Public domain W3C validator