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

Theorem f1ofo 6792
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 6791 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 499 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5633  Fun wfun 6491  ontowfo 6495  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1imacnv  6801  resin  6807  f1ococnv2  6812  fo00  6821  isoini  7284  isofrlem  7286  isoselem  7287  ncanth  7312  f1opw2  7609  f1dmex  7890  f1ovv  7891  f1oweALT  7906  wemoiso2  7908  curry1  8037  curry2  8040  smoiso2  8316  f1osetex  8798  bren  8894  brenOLD  8895  f1oeng  8912  en1  8966  en1OLD  8967  canth2  9075  domss2  9081  mapen  9086  ssenen  9096  dif1enlem  9101  dif1enlemOLD  9102  ssfiALT  9119  phplem2  9153  php3  9157  phplem4OLD  9165  php3OLD  9169  domunfican  9265  fiint  9269  f1fi  9284  f1opwfi  9301  mapfien  9345  supisolem  9410  ordiso2  9452  ordtypelem10  9464  oismo  9477  wdomref  9509  brwdom2  9510  unxpwdom2  9525  cantnflt2  9610  cantnfp1lem3  9617  wemapwe  9634  infxpenc2lem1  9956  fseqen  9964  infpwfien  9999  infmap2  10155  ackbij2  10180  cff1  10195  cofsmo  10206  infpssr  10245  enfin2i  10258  fin23lem27  10265  enfin1ai  10321  fin1a2lem7  10343  axcclem  10394  ttukeylem1  10446  fpwwe2lem5  10572  fpwwe2lem8  10575  canthp1lem2  10590  tskuni  10720  gruen  10749  cnexALT  12912  fiinfnf1o  14251  hasheqf1oi  14252  hashfacen  14352  hashfacenOLD  14353  fsumf1o  15609  fsumss  15611  fprodf1o  15830  fprodss  15832  ruc  16126  unbenlem  16781  xpsfrn  17451  xpsbas  17455  xpsadd  17457  xpsmul  17458  xpssca  17459  xpsvsca  17460  xpsless  17461  xpsle  17462  imasmndf1  18596  sursubmefmnd  18707  imasgrpf1  18865  gicsubgen  19069  symgmov2  19170  symgextfo  19205  symgfixelsi  19218  giccyg  19678  gsumzres  19687  gsumzcl2  19688  gsumzf1o  19690  gsumzaddlem  19699  gsumconst  19712  gsumzmhm  19715  gsumzoppg  19722  dprdf1o  19812  gsumfsum  20867  znleval  20964  lmimlbs  21245  lbslcic  21250  coe1mul2lem2  21642  cmpfi  22762  idqtop  23060  basqtop  23065  tgqtop  23066  hmeontr  23123  hmeoimaf1o  23124  hmeoqtop  23129  cmphmph  23142  connhmph  23143  nrmhmph  23148  indishmph  23152  cmphaushmeo  23154  xpstps  23164  xpstopnlem2  23165  fmid  23314  tsmsf1o  23499  imasdsf1olem  23729  imasf1oxmet  23731  imasf1omet  23732  xpsdsfn  23733  imasf1oxms  23848  imasf1oms  23849  iccpnfhmeo  24311  cnheiborlem  24320  ovolctb  24857  ovolicc2lem4  24887  dyadmbl  24967  mbfimaopnlem  25022  itg1addlem4  25066  itg1addlem4OLD  25067  dvcnvrelem2  25385  dvcnvre  25386  deg1ldg  25460  deg1leb  25463  efifo  25906  logrn  25917  dvrelog  25995  efopnlem2  26015  fsumdvdsmul  26547  f1otrg  27816  axcontlem10  27925  edgusgrnbfin  28324  eupthvdres  29182  cnvunop  30863  counop  30866  idunop  30923  elunop2  30958  fmptco1f1o  31550  padct  31639  symgcom  31937  cycpmconjvlem  31993  cycpmconjslem2  32007  xrge0iifiso  32519  volmeas  32833  ballotlemro  33125  derangenlem  33768  subfacp1lem3  33779  subfacp1lem5  33781  erdsze2lem1  33800  cvmsss2  33871  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem9  36090  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem14  36095  poimirlem15  36096  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem24  36105  poimirlem25  36106  poimirlem29  36110  poimirlem31  36112  mblfinlem2  36119  ismtybndlem  36268  ismtyres  36270  diaintclN  39524  dibintclN  39633  mapdrn  40115  riccrng1  40706  ricdrng1  40720  dnnumch2  41375  kelac1  41393  lnmlmic  41418  pwslnmlem1  41422  pwfi2f1o  41426  gicabl  41429  imasgim  41430  isnumbasgrplem1  41431  ntrneifv2  42359  stoweidlem27  44275  fourierdlem20  44375  fourierdlem51  44405  fourierdlem52  44406  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem102  44456  fourierdlem114  44468  sge0f1o  44630  nnfoctbdjlem  44703  isomenndlem  44778  ovnsubaddlem1  44818  f1oresf1o2  45530  isomuspgrlem2d  46030
  Copyright terms: Public domain W3C validator