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

Theorem f1ofun 5490
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofun  |-  ( F : A -1-1-onto-> B  ->  Fun  F )

Proof of Theorem f1ofun
StepHypRef Expression
1 f1ofn 5489 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5357 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 15 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5265    Fn wfn 5266   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1orel  5491  fveqf1o  5822  isofrlem  5853  isofr  5855  isose  5856  f1opw  6088  xpcomco  6968  f1opwfi  7175  mapfien  7415  isercolllem2  12155  isercoll  12157  unbenlem  12971  tgqtop  17419  hmeontr  17476  reghmph  17500  nrmhmph  17501  tgpconcompeqg  17810  cnheiborlem  18468  dfrelog  19939  dvloglem  20011  logf1o2  20013  ballotlemrv  23094  tpr2rico  23311  gsumpropd2lem  23394  subfacp1lem2a  23726  subfacp1lem2b  23727  subfacp1lem5  23730  eupares  23914  eupap1  23915  axcontlem9  24672  axcontlem10  24673  domrancur1c  25305  ismtyres  26635  diaclN  31862  dia1elN  31866  diaintclN  31870  docaclN  31936  dibintclN  31979
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5274  df-f 5275  df-f1 5276  df-f1o 5278
  Copyright terms: Public domain W3C validator