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

Theorem dffo2 5624
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 5620 . . 3  |-  ( F : A -onto-> B  ->  F : A --> B )
2 forn 5623 . . 3  |-  ( F : A -onto-> B  ->  ran  F  =  B )
31, 2jca 519 . 2  |-  ( F : A -onto-> B  -> 
( F : A --> B  /\  ran  F  =  B ) )
4 ffn 5558 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
5 df-fo 5427 . . . 4  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
65biimpri 198 . . 3  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  F : A -onto-> B )
74, 6sylan 458 . 2  |-  ( ( F : A --> B  /\  ran  F  =  B )  ->  F : A -onto-> B )
83, 7impbii 181 1  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1649   ran crn 4846    Fn wfn 5416   -->wf 5417   -onto->wfo 5419
This theorem is referenced by:  foco  5630  foconst  5631  dff1o5  5650  dffo3  5851  dffo4  5852  exfo  5854  fo1stres  6337  fo2ndres  6338  fo2ndf  6420  cantnf  7613  hsmexlem2  8271  1fv  11083  setcepi  14206  odf1o1  15169  efgsfo  15334  pjfo  16905  xrhmeo  18932  fargshiftfo  21586  grpofo  21748  cnpcon  24878  lnmepi  27059
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302  df-f 5425  df-fo 5427
  Copyright terms: Public domain W3C validator