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

Theorem f1ofo 5479
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 5478 . 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 4688   Fun wfun 5249   -onto->wfo 5253   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1imacnv  5489  resin  5495  f1ococnv2  5500  fo00  5509  f1dmex  5751  isoini  5835  isofrlem  5837  isoselem  5838  f1oweALT  5851  wemoiso2  5856  f1opw2  6071  curry1  6210  curry2  6213  ncanth  6295  smoiso2  6386  bren  6871  f1oeng  6880  en1  6928  canth2  7014  domss2  7020  mapen  7025  ssenen  7035  phplem4  7043  php3  7047  ssfi  7083  domunfican  7129  fiint  7133  f1fi  7143  f1opwfi  7159  supisolem  7221  ordiso2  7230  ordtypelem10  7242  oismo  7255  wdomref  7286  brwdom2  7287  unxpwdom2  7302  cantnflt2  7374  cantnfp1lem3  7382  mapfien  7399  wemapwe  7400  infxpenc2lem1  7646  fseqen  7654  infpwfien  7689  infmap2  7844  ackbij2  7869  cff1  7884  cofsmo  7895  infpssr  7934  enfin2i  7947  fin23lem27  7954  enfin1ai  8010  fin1a2lem7  8032  axcclem  8083  ttukeylem1  8136  fpwwe2lem6  8257  fpwwe2lem9  8260  canthp1lem2  8275  tskuni  8405  gruen  8434  cnexALT  10350  hashfacen  11392  fsumf1o  12196  fsumss  12198  ruc  12521  unbenlem  12955  xpsfrn  13471  xpsbas  13476  xpsadd  13478  xpsmul  13479  xpssca  13480  xpsvsca  13481  xpsless  13482  xpsle  13483  imasmndf1  14411  imasgrpf1  14612  gicsubgen  14742  giccyg  15186  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  dprdf1o  15267  coe1mul2lem2  16345  gsumfsum  16439  znleval  16508  cmpfi  17135  idqtop  17397  basqtop  17402  tgqtop  17403  hmeontr  17460  hmeoimaf1o  17461  hmeoqtop  17466  cmphmph  17479  conhmph  17480  nrmhmph  17485  indishmph  17489  cmphaushmeo  17491  xpstps  17501  xpstopnlem2  17502  fmid  17655  tsmsf1o  17827  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  xpsdsfn  17941  imasf1oxms  18035  imasf1oms  18036  iccpnfhmeo  18443  cnheiborlem  18452  ovolctb  18849  ovolicc2lem4  18879  dyadmbl  18955  mbfimaopnlem  19010  itg1addlem4  19054  dvcnvrelem2  19365  dvcnvre  19366  deg1ldg  19478  deg1leb  19481  efifo  19909  logrn  19916  dvrelog  19984  efopnlem2  20004  fsumdvdsmul  20435  cnvunop  22498  counop  22501  idunop  22558  elunop2  22593  ballotlemro  23081  xrge0iifiso  23317  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  erdsze2lem1  23734  cvmsss2  23805  eupares  23899  eupath2lem3  23903  eupath2  23904  axcontlem10  24601  f1ofi  25070  domrancur1c  25202  rngapm  25370  ismtybndlem  26530  ismtyres  26532  dnnumch2  27142  kelac1  27161  lnmlmic  27186  pwslnmlem1  27194  pwfi2f1o  27260  gicabl  27263  imasgim  27264  isnumbasgrplem1  27266  lmimlbs  27306  lbslcic  27311  stoweidlem27  27776  diaintclN  31248  dibintclN  31357  mapdrn  31839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator