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

Theorem f1ofo 5684
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 5683 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
21simplbi 448 1  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4880   Fun wfun 5451   -onto->wfo 5455   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1imacnv  5694  resin  5700  f1ococnv2  5705  fo00  5714  f1dmex  5974  isoini  6061  isofrlem  6063  isoselem  6064  f1oweALT  6077  wemoiso2  6082  f1opw2  6301  curry1  6441  curry2  6444  ncanth  6543  smoiso2  6634  bren  7120  f1oeng  7129  en1  7177  canth2  7263  domss2  7269  mapen  7274  ssenen  7284  phplem4  7292  php3  7296  ssfi  7332  domunfican  7382  fiint  7386  f1fi  7396  f1opwfi  7413  supisolem  7478  ordiso2  7487  ordtypelem10  7499  oismo  7512  wdomref  7543  brwdom2  7544  unxpwdom2  7559  cantnflt2  7631  cantnfp1lem3  7639  mapfien  7656  wemapwe  7657  infxpenc2lem1  7905  fseqen  7913  infpwfien  7948  infmap2  8103  ackbij2  8128  cff1  8143  cofsmo  8154  infpssr  8193  enfin2i  8206  fin23lem27  8213  enfin1ai  8269  fin1a2lem7  8291  axcclem  8342  ttukeylem1  8394  fpwwe2lem6  8515  fpwwe2lem9  8518  canthp1lem2  8533  tskuni  8663  gruen  8692  cnexALT  10613  1fv  11125  fiinfnf1o  11639  hashfacen  11708  fsumf1o  12522  fsumss  12524  ruc  12847  unbenlem  13281  xpsfrn  13799  xpsbas  13804  xpsadd  13806  xpsmul  13807  xpssca  13808  xpsvsca  13809  xpsless  13810  xpsle  13811  imasmndf1  14739  imasgrpf1  14940  gicsubgen  15070  giccyg  15514  gsumval3  15519  gsumzres  15522  gsumzcl  15523  gsumzf1o  15524  gsumzaddlem  15531  gsumconst  15537  gsumzmhm  15538  gsumzoppg  15544  dprdf1o  15595  coe1mul2lem2  16666  gsumfsum  16771  znleval  16840  cmpfi  17476  idqtop  17743  basqtop  17748  tgqtop  17749  hmeontr  17806  hmeoimaf1o  17807  hmeoqtop  17812  cmphmph  17825  conhmph  17826  nrmhmph  17831  indishmph  17835  cmphaushmeo  17837  xpstps  17847  xpstopnlem2  17848  fmid  17997  tsmsf1o  18179  imasdsf1olem  18408  imasf1oxmet  18410  imasf1omet  18411  xpsdsfn  18412  imasf1oxms  18524  imasf1oms  18525  iccpnfhmeo  18975  cnheiborlem  18984  ovolctb  19391  ovolicc2lem4  19421  dyadmbl  19497  mbfimaopnlem  19550  itg1addlem4  19594  dvcnvrelem2  19907  dvcnvre  19908  deg1ldg  20020  deg1leb  20023  efifo  20454  logrn  20461  dvrelog  20533  efopnlem2  20553  fsumdvdsmul  20985  edgusgranbfin  21464  eupatrl  21695  eupares  21702  eupath2lem3  21706  eupath2  21707  cnvunop  23426  counop  23429  idunop  23486  elunop2  23521  xrge0iifiso  24326  volmeas  24592  ballotlemro  24785  derangenlem  24862  subfacp1lem3  24873  subfacp1lem5  24875  erdsze2lem1  24894  cvmsss2  24966  fprodf1o  25277  fprodss  25279  axcontlem10  25917  mblfinlem2  26256  ismtybndlem  26529  ismtyres  26531  dnnumch2  27134  kelac1  27152  lnmlmic  27177  pwslnmlem1  27185  pwfi2f1o  27251  gicabl  27254  imasgim  27255  isnumbasgrplem1  27257  lmimlbs  27297  lbslcic  27302  stoweidlem27  27766  diaintclN  31930  dibintclN  32039  mapdrn  32521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464
  Copyright terms: Public domain W3C validator