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

Theorem dffo2 5722
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 5718 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5721 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 532 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5657 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5522 . . . 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 1370   ran crn 4939    Fn wfn 5511   -->wf 5512   -onto->wfo 5514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440  df-f 5520  df-fo 5522
This theorem is referenced by:  foco  5728  foconst  5729  dff1o5  5748  dffo3  5957  dffo4  5958  exfo  5960  fo1stres  6700  fo2ndres  6701  fo2ndf  6779  cantnf  8002  cantnfOLD  8024  hsmexlem2  8697  1fv  11633  setcepi  15058  odf1o1  16175  efgsfo  16340  pjfo  18249  xrhmeo  20634  fargshiftfo  23659  grpofo  23821  cnpcon  27253  lnmepi  29576
  Copyright terms: Public domain W3C validator