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

Theorem dffo2 5660
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 5656 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5659 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 520 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5594 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5463 . . . 4  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
65biimpri 199 . . 3  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  F : A -onto-> B )
74, 6sylan 459 . 2  |-  ( ( F : A --> B  /\  ran  F  =  B )  ->  F : A -onto-> B )
83, 7impbii 182 1  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653   ran crn 4882    Fn wfn 5452   -->wf 5453   -onto->wfo 5455
This theorem is referenced by:  foco  5666  foconst  5667  dff1o5  5686  dffo3  5887  dffo4  5888  exfo  5890  fo1stres  6373  fo2ndres  6374  fo2ndf  6456  cantnf  7652  hsmexlem2  8312  1fv  11125  setcepi  14248  odf1o1  15211  efgsfo  15376  pjfo  16947  xrhmeo  18976  fargshiftfo  21630  grpofo  21792  cnpcon  24922  lnmepi  27174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5461  df-fo 5463
  Copyright terms: Public domain W3C validator