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

Theorem f1ofo 5495
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 5494 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
21simplbi 446 1  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4704   Fun wfun 5265   -onto->wfo 5269   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1imacnv  5505  resin  5511  f1ococnv2  5516  fo00  5525  f1dmex  5767  isoini  5851  isofrlem  5853  isoselem  5854  f1oweALT  5867  wemoiso2  5872  f1opw2  6087  curry1  6226  curry2  6229  ncanth  6311  smoiso2  6402  bren  6887  f1oeng  6896  en1  6944  canth2  7030  domss2  7036  mapen  7041  ssenen  7051  phplem4  7059  php3  7063  ssfi  7099  domunfican  7145  fiint  7149  f1fi  7159  f1opwfi  7175  supisolem  7237  ordiso2  7246  ordtypelem10  7258  oismo  7271  wdomref  7302  brwdom2  7303  unxpwdom2  7318  cantnflt2  7390  cantnfp1lem3  7398  mapfien  7415  wemapwe  7416  infxpenc2lem1  7662  fseqen  7670  infpwfien  7705  infmap2  7860  ackbij2  7885  cff1  7900  cofsmo  7911  infpssr  7950  enfin2i  7963  fin23lem27  7970  enfin1ai  8026  fin1a2lem7  8048  axcclem  8099  ttukeylem1  8152  fpwwe2lem6  8273  fpwwe2lem9  8276  canthp1lem2  8291  tskuni  8421  gruen  8450  cnexALT  10366  hashfacen  11408  fsumf1o  12212  fsumss  12214  ruc  12537  unbenlem  12971  xpsfrn  13487  xpsbas  13492  xpsadd  13494  xpsmul  13495  xpssca  13496  xpsvsca  13497  xpsless  13498  xpsle  13499  imasmndf1  14427  imasgrpf1  14628  gicsubgen  14758  giccyg  15202  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  dprdf1o  15283  coe1mul2lem2  16361  gsumfsum  16455  znleval  16524  cmpfi  17151  idqtop  17413  basqtop  17418  tgqtop  17419  hmeontr  17476  hmeoimaf1o  17477  hmeoqtop  17482  cmphmph  17495  conhmph  17496  nrmhmph  17501  indishmph  17505  cmphaushmeo  17507  xpstps  17517  xpstopnlem2  17518  fmid  17671  tsmsf1o  17843  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  xpsdsfn  17957  imasf1oxms  18051  imasf1oms  18052  iccpnfhmeo  18459  cnheiborlem  18468  ovolctb  18865  ovolicc2lem4  18895  dyadmbl  18971  mbfimaopnlem  19026  itg1addlem4  19070  dvcnvrelem2  19381  dvcnvre  19382  deg1ldg  19494  deg1leb  19497  efifo  19925  logrn  19932  dvrelog  20000  efopnlem2  20020  fsumdvdsmul  20451  cnvunop  22514  counop  22517  idunop  22574  elunop2  22609  ballotlemro  23097  xrge0iifiso  23332  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  erdsze2lem1  23749  cvmsss2  23820  eupares  23914  eupath2lem3  23918  eupath2  23919  fprodf1o  24172  axcontlem10  24673  f1ofi  25173  domrancur1c  25305  rngapm  25473  ismtybndlem  26633  ismtyres  26635  dnnumch2  27245  kelac1  27264  lnmlmic  27289  pwslnmlem1  27297  pwfi2f1o  27363  gicabl  27366  imasgim  27367  isnumbasgrplem1  27369  lmimlbs  27409  lbslcic  27414  stoweidlem27  27879  eupatrl  28385  diaintclN  31870  dibintclN  31979  mapdrn  32461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278
  Copyright terms: Public domain W3C validator