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

Theorem dffo2 5455
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 5451 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5454 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 518 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5389 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5261 . . . 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 1623   ran crn 4690    Fn wfn 5250   -->wf 5251   -onto->wfo 5253
This theorem is referenced by:  foco  5461  foconst  5462  dff1o5  5481  dffo3  5675  dffo4  5676  exfo  5678  fo1stres  6143  fo2ndres  6144  cantnf  7395  hsmexlem2  8053  setcepi  13920  odf1o1  14883  efgsfo  15048  pjfo  16615  xrhmeo  18444  grpofo  20866  cnpcon  23761  grpodivfo  25374  lnmepi  27183
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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-fo 5261
  Copyright terms: Public domain W3C validator