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

Theorem f1ofo 5623
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 5622 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
21simplbi 447 1  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4819   Fun wfun 5390   -onto->wfo 5394   -1-1-onto->wf1o 5395
This theorem is referenced by:  f1imacnv  5633  resin  5639  f1ococnv2  5644  fo00  5653  f1dmex  5912  isoini  5999  isofrlem  6001  isoselem  6002  f1oweALT  6015  wemoiso2  6020  f1opw2  6239  curry1  6379  curry2  6382  ncanth  6478  smoiso2  6569  bren  7055  f1oeng  7064  en1  7112  canth2  7198  domss2  7204  mapen  7209  ssenen  7219  phplem4  7227  php3  7231  ssfi  7267  domunfican  7317  fiint  7321  f1fi  7331  f1opwfi  7347  supisolem  7410  ordiso2  7419  ordtypelem10  7431  oismo  7444  wdomref  7475  brwdom2  7476  unxpwdom2  7491  cantnflt2  7563  cantnfp1lem3  7571  mapfien  7588  wemapwe  7589  infxpenc2lem1  7835  fseqen  7843  infpwfien  7878  infmap2  8033  ackbij2  8058  cff1  8073  cofsmo  8084  infpssr  8123  enfin2i  8136  fin23lem27  8143  enfin1ai  8199  fin1a2lem7  8221  axcclem  8272  ttukeylem1  8324  fpwwe2lem6  8445  fpwwe2lem9  8448  canthp1lem2  8463  tskuni  8593  gruen  8622  cnexALT  10542  1fv  11052  fiinfnf1o  11563  hashfacen  11632  fsumf1o  12446  fsumss  12448  ruc  12771  unbenlem  13205  xpsfrn  13723  xpsbas  13728  xpsadd  13730  xpsmul  13731  xpssca  13732  xpsvsca  13733  xpsless  13734  xpsle  13735  imasmndf1  14663  imasgrpf1  14864  gicsubgen  14994  giccyg  15438  gsumval3  15443  gsumzres  15446  gsumzcl  15447  gsumzf1o  15448  gsumzaddlem  15455  gsumconst  15461  gsumzmhm  15462  gsumzoppg  15468  dprdf1o  15519  coe1mul2lem2  16590  gsumfsum  16691  znleval  16760  cmpfi  17395  idqtop  17661  basqtop  17666  tgqtop  17667  hmeontr  17724  hmeoimaf1o  17725  hmeoqtop  17730  cmphmph  17743  conhmph  17744  nrmhmph  17749  indishmph  17753  cmphaushmeo  17755  xpstps  17765  xpstopnlem2  17766  fmid  17915  tsmsf1o  18097  imasdsf1olem  18313  imasf1oxmet  18315  imasf1omet  18316  xpsdsfn  18317  imasf1oxms  18411  imasf1oms  18412  iccpnfhmeo  18843  cnheiborlem  18852  ovolctb  19255  ovolicc2lem4  19285  dyadmbl  19361  mbfimaopnlem  19416  itg1addlem4  19460  dvcnvrelem2  19771  dvcnvre  19772  deg1ldg  19884  deg1leb  19887  efifo  20318  logrn  20325  dvrelog  20397  efopnlem2  20417  fsumdvdsmul  20849  edgusgranbfin  21327  eupatrl  21540  eupares  21547  eupath2lem3  21551  eupath2  21552  cnvunop  23271  counop  23274  idunop  23331  elunop2  23366  xrge0iifiso  24127  volmeas  24383  ballotlemro  24561  derangenlem  24638  subfacp1lem3  24649  subfacp1lem5  24651  erdsze2lem1  24670  cvmsss2  24742  fprodf1o  25053  fprodss  25055  axcontlem10  25628  ismtybndlem  26208  ismtyres  26210  dnnumch2  26813  kelac1  26832  lnmlmic  26857  pwslnmlem1  26865  pwfi2f1o  26931  gicabl  26934  imasgim  26935  isnumbasgrplem1  26937  lmimlbs  26977  lbslcic  26982  stoweidlem27  27446  diaintclN  31175  dibintclN  31284  mapdrn  31766
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403
  Copyright terms: Public domain W3C validator