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

Theorem f1ofo 6042
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 6041 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 475 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5027  Fun wfun 5784  ontowfo 5788  1-1-ontowf1o 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797
This theorem is referenced by:  f1imacnv  6051  resin  6056  f1ococnv2  6061  fo00  6069  isoini  6466  isofrlem  6468  isoselem  6469  ncanth  6487  f1opw2  6764  f1dmex  7007  f1ovv  7008  f1oweALT  7021  wemoiso2  7023  curry1  7134  curry2  7137  smoiso2  7331  bren  7828  f1oeng  7838  en1  7887  canth2  7976  domss2  7982  mapen  7987  ssenen  7997  phplem4  8005  php3  8009  ssfi  8043  domunfican  8096  fiint  8100  f1fi  8114  f1opwfi  8131  mapfien  8174  supisolem  8240  ordiso2  8281  ordtypelem10  8293  oismo  8306  wdomref  8338  brwdom2  8339  unxpwdom2  8354  cantnflt2  8431  cantnfp1lem3  8438  wemapwe  8455  infxpenc2lem1  8703  fseqen  8711  infpwfien  8746  infmap2  8901  ackbij2  8926  cff1  8941  cofsmo  8952  infpssr  8991  enfin2i  9004  fin23lem27  9011  enfin1ai  9067  fin1a2lem7  9089  axcclem  9140  ttukeylem1  9192  fpwwe2lem6  9314  fpwwe2lem9  9317  canthp1lem2  9332  tskuni  9462  gruen  9491  cnexALT  11663  fiinfnf1o  12955  hasheqf1oi  12957  hashfacen  13050  fsumf1o  14250  fsumss  14252  fprodf1o  14464  fprodss  14466  ruc  14760  unbenlem  15399  xpsfrn  16001  xpsbas  16006  xpsadd  16008  xpsmul  16009  xpssca  16010  xpsvsca  16011  xpsless  16012  xpsle  16013  imasmndf1  17101  imasgrpf1  17304  gicsubgen  17493  symgmov2  17585  symgextfo  17614  symgfixelsi  17627  giccyg  18073  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumconst  18106  gsumzmhm  18109  gsumzoppg  18116  dprdf1o  18203  coe1mul2lem2  19408  gsumfsum  19581  znleval  19670  lmimlbs  19942  lbslcic  19947  cmpfi  20969  idqtop  21267  basqtop  21272  tgqtop  21273  hmeontr  21330  hmeoimaf1o  21331  hmeoqtop  21336  cmphmph  21349  conhmph  21350  nrmhmph  21355  indishmph  21359  cmphaushmeo  21361  xpstps  21371  xpstopnlem2  21372  fmid  21522  tsmsf1o  21706  imasdsf1olem  21936  imasf1oxmet  21938  imasf1omet  21939  xpsdsfn  21940  imasf1oxms  22052  imasf1oms  22053  iccpnfhmeo  22500  cnheiborlem  22509  ovolctb  23010  ovolicc2lem4  23040  dyadmbl  23119  mbfimaopnlem  23173  itg1addlem4  23217  dvcnvrelem2  23530  dvcnvre  23531  deg1ldg  23601  deg1leb  23604  efifo  24042  logrn  24054  dvrelog  24128  efopnlem2  24148  fsumdvdsmul  24666  f1otrg  25497  axcontlem10  25599  edgusgranbfin  25773  eupatrl  26289  eupares  26296  eupath2lem3  26300  eupath2  26301  cnvunop  27955  counop  27958  idunop  28015  elunop2  28050  padct  28679  xrge0iifiso  29103  volmeas  29415  ballotlemro  29705  derangenlem  30201  subfacp1lem3  30212  subfacp1lem5  30214  erdsze2lem1  30233  cvmsss2  30304  poimirlem1  32374  poimirlem2  32375  poimirlem3  32376  poimirlem4  32377  poimirlem5  32378  poimirlem6  32379  poimirlem7  32380  poimirlem9  32382  poimirlem10  32383  poimirlem11  32384  poimirlem12  32385  poimirlem14  32387  poimirlem15  32388  poimirlem16  32389  poimirlem17  32390  poimirlem19  32392  poimirlem20  32393  poimirlem22  32395  poimirlem23  32396  poimirlem24  32397  poimirlem25  32398  poimirlem29  32402  poimirlem31  32404  mblfinlem2  32411  ismtybndlem  32569  ismtyres  32571  diaintclN  35159  dibintclN  35268  mapdrn  35750  dnnumch2  36427  kelac1  36445  lnmlmic  36470  pwslnmlem1  36474  pwfi2f1o  36478  gicabl  36481  imasgim  36482  isnumbasgrplem1  36484  ntrneifv2  37192  stoweidlem27  38714  fourierdlem20  38814  fourierdlem51  38844  fourierdlem52  38845  fourierdlem63  38856  fourierdlem64  38857  fourierdlem65  38858  fourierdlem102  38895  fourierdlem114  38907  sge0f1o  39069  nnfoctbdjlem  39142  isomenndlem  39214  ovnsubaddlem1  39254  edgusgrnbfin  40593  eupthvdres  41395
  Copyright terms: Public domain W3C validator