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

Theorem f1ofun 5668
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 5667 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5534 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 16 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5440    Fn wfn 5441   -1-1-onto->wf1o 5445
This theorem is referenced by:  f1orel  5669  fveqf1o  6021  isofrlem  6052  isofr  6054  isose  6055  f1opw  6291  xpcomco  7190  f1opwfi  7402  mapfien  7645  isercolllem2  12451  isercoll  12453  unbenlem  13268  tgqtop  17736  hmeontr  17793  reghmph  17817  nrmhmph  17818  tgpconcompeqg  18133  cnheiborlem  18971  dfrelog  20455  dvloglem  20531  logf1o2  20533  eupares  21689  eupap1  21690  gsumpropd2lem  24212  tpr2rico  24302  ballotlemrv  24769  subfacp1lem2a  24858  subfacp1lem2b  24859  subfacp1lem5  24862  axcontlem9  25903  axcontlem10  25904  ismtyres  26508  diaclN  31785  dia1elN  31789  diaintclN  31793  docaclN  31859  dibintclN  31902
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 178  df-an 361  df-fn 5449  df-f 5450  df-f1 5451  df-f1o 5453
  Copyright terms: Public domain W3C validator