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

Theorem f1ofo 5640
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 5639 . 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 4836   Fun wfun 5407   -onto->wfo 5411   -1-1-onto->wf1o 5412
This theorem is referenced by:  f1imacnv  5650  resin  5656  f1ococnv2  5661  fo00  5670  f1dmex  5930  isoini  6017  isofrlem  6019  isoselem  6020  f1oweALT  6033  wemoiso2  6038  f1opw2  6257  curry1  6397  curry2  6400  ncanth  6499  smoiso2  6590  bren  7076  f1oeng  7085  en1  7133  canth2  7219  domss2  7225  mapen  7230  ssenen  7240  phplem4  7248  php3  7252  ssfi  7288  domunfican  7338  fiint  7342  f1fi  7352  f1opwfi  7368  supisolem  7431  ordiso2  7440  ordtypelem10  7452  oismo  7465  wdomref  7496  brwdom2  7497  unxpwdom2  7512  cantnflt2  7584  cantnfp1lem3  7592  mapfien  7609  wemapwe  7610  infxpenc2lem1  7856  fseqen  7864  infpwfien  7899  infmap2  8054  ackbij2  8079  cff1  8094  cofsmo  8105  infpssr  8144  enfin2i  8157  fin23lem27  8164  enfin1ai  8220  fin1a2lem7  8242  axcclem  8293  ttukeylem1  8345  fpwwe2lem6  8466  fpwwe2lem9  8469  canthp1lem2  8484  tskuni  8614  gruen  8643  cnexALT  10564  1fv  11075  fiinfnf1o  11589  hashfacen  11658  fsumf1o  12472  fsumss  12474  ruc  12797  unbenlem  13231  xpsfrn  13749  xpsbas  13754  xpsadd  13756  xpsmul  13757  xpssca  13758  xpsvsca  13759  xpsless  13760  xpsle  13761  imasmndf1  14689  imasgrpf1  14890  gicsubgen  15020  giccyg  15464  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  dprdf1o  15545  coe1mul2lem2  16616  gsumfsum  16721  znleval  16790  cmpfi  17425  idqtop  17691  basqtop  17696  tgqtop  17697  hmeontr  17754  hmeoimaf1o  17755  hmeoqtop  17760  cmphmph  17773  conhmph  17774  nrmhmph  17779  indishmph  17783  cmphaushmeo  17785  xpstps  17795  xpstopnlem2  17796  fmid  17945  tsmsf1o  18127  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  xpsdsfn  18360  imasf1oxms  18472  imasf1oms  18473  iccpnfhmeo  18923  cnheiborlem  18932  ovolctb  19339  ovolicc2lem4  19369  dyadmbl  19445  mbfimaopnlem  19500  itg1addlem4  19544  dvcnvrelem2  19855  dvcnvre  19856  deg1ldg  19968  deg1leb  19971  efifo  20402  logrn  20409  dvrelog  20481  efopnlem2  20501  fsumdvdsmul  20933  edgusgranbfin  21412  eupatrl  21643  eupares  21650  eupath2lem3  21654  eupath2  21655  cnvunop  23374  counop  23377  idunop  23434  elunop2  23469  xrge0iifiso  24274  volmeas  24540  ballotlemro  24733  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  erdsze2lem1  24842  cvmsss2  24914  fprodf1o  25225  fprodss  25227  axcontlem10  25816  mblfinlem  26143  ismtybndlem  26405  ismtyres  26407  dnnumch2  27010  kelac1  27029  lnmlmic  27054  pwslnmlem1  27062  pwfi2f1o  27128  gicabl  27131  imasgim  27132  isnumbasgrplem1  27134  lmimlbs  27174  lbslcic  27179  stoweidlem27  27643  diaintclN  31541  dibintclN  31650  mapdrn  32132
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420
  Copyright terms: Public domain W3C validator