Theorem f1ofo 6862

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)

Assertion

Ref	Expression
f1ofo	⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶onto𝐵)

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		dff1o3 6861	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶onto𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → 𝐹:𝐴⟶onto𝐵)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5657  Fun wfun 6560  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1imacnv  6871  resin  6877  f1ococnv2  6883  fo00  6892  f1ounsn  7311  f1ocoima  7342  isoini  7377  isofrlem  7379  isoselem  7380  ncanth  7406  f1opw2  7708  f1dmex  8003  f1ovv  8004  f1oweALT  8018  wemoiso2  8020  mptcnfimad  8032  curry1  8152  curry2  8155  smoiso2  8415  f1osetex  8919  bren  9021  f1oeng  9035  en1  9089  canth2  9187  domss2  9193  mapen  9198  ssenen  9208  dif1enlem  9213  ssfiALT  9227  phplem2  9258  php3  9262  f1fi  9344  domunfican  9351  fiint  9356  f1opwfi  9383  mapfien  9437  supisolem  9503  ordiso2  9546  ordtypelem10  9558  oismo  9571  wdomref  9603  brwdom2  9604  unxpwdom2  9619  cantnflt2  9711  cantnfp1lem3  9718  wemapwe  9735  infxpenc2lem1  10137  fseqen  10145  infpwfien  10180  infmap2  10334  ackbij2  10359  cff1  10375  cofsmo  10386  infpssr  10425  enfin2i  10438  fin23lem27  10445  enfin1ai  10501  fin1a2lem7  10523  axcclem  10574  ttukeylem1  10626  fpwwe2lem5  10759  fpwwe2lem8  10762  canthp1lem2  10777  tskuni  10907  gruen  10936  cnexALT  13154  fiinfnf1o  14535  hasheqf1oi  14536  hashfacen  14640  fsumf1o  15933  fsumss  15935  fprodf1o  16157  fprodss  16159  ruc  16455  unbenlem  17130  xpsfrn  17790  xpsbas  17794  xpsadd  17796  xpsmul  17797  xpssca  17798  xpsvsca  17799  xpsless  17800  xpsle  17801  imasmndf1  19020  sursubmefmnd  19142  imasgrpf1  19317  imasgim  19534  gicsubgen  19544  symgmov2  19653  symgextfo  19687  symgfixelsi  19700  giccyg  20165  gsumzres  20174  gsumzcl2  20175  gsumzf1o  20177  gsumzaddlem  20186  gsumconst  20199  gsumzmhm  20202  gsumzoppg  20209  dprdf1o  20299  imasrngf1  20451  imasringf1  20612  gsumfsum  21794  znleval  21915  lmimlbs  22197  lbslcic  22202  coe1mul2lem2  22642  cmpfi  23781  idqtop  24080  basqtop  24085  tgqtop  24086  hmeontr  24143  hmeoimaf1o  24144  hmeoqtop  24149  cmphmph  24162  connhmph  24163  nrmhmph  24168  indishmph  24172  cmphaushmeo  24174  xpstps  24184  xpstopnlem2  24185  fmid  24334  tsmsf1o  24519  imasdsf1olem  24747  imasf1oxmet  24749  imasf1omet  24750  xpsdsfn  24751  imasf1oxms  24863  imasf1oms  24864  iccpnfhmeo  25321  cnheiborlem  25330  ovolctb  25866  ovolicc2lem4  25896  dyadmbl  25976  mbfimaopnlem  26031  itg1addlem4  26075  dvcnvrelem2  26393  dvcnvre  26394  deg1ldg  26465  deg1leb  26468  efifo  26932  logrn  26943  dvrelog  27022  efopnlem2  27042  fsumdvdsmul  27579  f1otrg  29505  axcontlem10  29608  edgusgrnbfin  30011  eupthvdres  30893  cnvunop  32577  counop  32580  idunop  32637  elunop2  32672  fmptco1f1o  33325  padct  33407  mndlactf1o  33690  mndractf1o  33691  symgcom  33743  cycpmconjvlem  33801  cycpmconjslem2  33815  1arithidomlem2  34172  esplysply  34314  xrge0iifiso  34678  volmeas  34975  ballotlemro  35266  jf1o  36052  prconf1acwevd  36089  vonf1oonfo  36090  derangenlem  36144  subfacp1lem3  36155  subfacp1lem5  36157  erdsze2lem1  36176  cvmsss2  36247  poimirlem1  38807  poimirlem2  38808  poimirlem3  38809  poimirlem4  38810  poimirlem5  38811  poimirlem6  38812  poimirlem7  38813  poimirlem9  38815  poimirlem10  38816  poimirlem11  38817  poimirlem12  38818  poimirlem14  38820  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem29  38835  poimirlem31  38837  mblfinlem2  38844  ismtybndlem  39006  ismtyres  39008  diaintclN  42381  dibintclN  42490  mapdrn  42972  aks6d1c1p5  43428  riccrng1  43848  ricdrng1  43858  dnnumch2  44318  kelac1  44331  lnmlmic  44356  pwslnmlem1  44360  pwfi2f1o  44364  gicabl  44367  isnumbasgrplem1  44368  ntrneifv2  45341  fingrphf  46300  stoweidlem27  47310  fourierdlem20  47410  fourierdlem51  47440  fourierdlem52  47441  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem102  47491  fourierdlem114  47503  sge0f1o  47665  nnfoctbdjlem  47738  isomenndlem  47813  ovnsubaddlem1  47853  3f1oss1  48418  f1oresf1o2  48634  grimuhgr  49258  grimcnv  49259  isuspgrimlem  49266  grimedg  49306  isubgr3stgrlem8  49344  tposres3  50325  uptrlem1  50657  lmdran  51185  cmdlan  51186