Theorem f1ofo 6837

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

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5650  Fun wfun 6537  –onto→wfo 6541  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-cleq 2752  df-ss 3897  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  f1imacnv  6846  resin  6852  f1ococnv2  6857  fo00  6866  f1ounsn  7284  f1ocoima  7315  isoini  7350  isofrlem  7352  isoselem  7353  ncanth  7379  f1opw2  7680  f1dmex  7973  f1ovv  7974  f1oweALT  7988  wemoiso2  7990  mptcnfimad  8002  curry1  8122  curry2  8125  smoiso2  8385  f1osetex  8889  bren  8991  f1oeng  9005  en1  9059  canth2  9157  domss2  9163  mapen  9168  ssenen  9178  dif1enlem  9183  ssfiALT  9197  phplem2  9228  php3  9232  f1fi  9314  domunfican  9321  fiint  9326  f1opwfi  9353  mapfien  9407  supisolem  9473  ordiso2  9516  ordtypelem10  9528  oismo  9541  wdomref  9573  brwdom2  9574  unxpwdom2  9589  cantnflt2  9681  cantnfp1lem3  9688  wemapwe  9705  infxpenc2lem1  10105  fseqen  10113  infpwfien  10148  infmap2  10302  ackbij2  10327  cff1  10343  cofsmo  10354  infpssr  10393  enfin2i  10406  fin23lem27  10413  enfin1ai  10469  fin1a2lem7  10491  axcclem  10542  ttukeylem1  10594  fpwwe2lem5  10727  fpwwe2lem8  10730  canthp1lem2  10745  tskuni  10875  gruen  10904  cnexALT  13121  fiinfnf1o  14501  hasheqf1oi  14502  hashfacen  14606  fsumf1o  15898  fsumss  15900  fprodf1o  16122  fprodss  16124  ruc  16420  unbenlem  17095  xpsfrn  17749  xpsbas  17753  xpsadd  17755  xpsmul  17756  xpssca  17757  xpsvsca  17758  xpsless  17759  xpsle  17760  imasmndf1  18979  sursubmefmnd  19101  imasgrpf1  19276  gicsubgen  19502  symgmov2  19611  symgextfo  19645  symgfixelsi  19658  giccyg  20123  gsumzres  20132  gsumzcl2  20133  gsumzf1o  20135  gsumzaddlem  20144  gsumconst  20157  gsumzmhm  20160  gsumzoppg  20167  dprdf1o  20257  imasrngf1  20409  imasringf1  20570  gsumfsum  21749  znleval  21869  lmimlbs  22151  lbslcic  22156  coe1mul2lem2  22596  cmpfi  23735  idqtop  24034  basqtop  24039  tgqtop  24040  hmeontr  24097  hmeoimaf1o  24098  hmeoqtop  24103  cmphmph  24116  connhmph  24117  nrmhmph  24122  indishmph  24126  cmphaushmeo  24128  xpstps  24138  xpstopnlem2  24139  fmid  24288  tsmsf1o  24473  imasdsf1olem  24701  imasf1oxmet  24703  imasf1omet  24704  xpsdsfn  24705  imasf1oxms  24817  imasf1oms  24818  iccpnfhmeo  25275  cnheiborlem  25284  ovolctb  25820  ovolicc2lem4  25850  dyadmbl  25930  mbfimaopnlem  25985  itg1addlem4  26029  dvcnvrelem2  26347  dvcnvre  26348  deg1ldg  26419  deg1leb  26422  efifo  26884  logrn  26895  dvrelog  26974  efopnlem2  26994  fsumdvdsmul  27531  f1otrg  29457  axcontlem10  29560  edgusgrnbfin  29963  eupthvdres  30845  cnvunop  32529  counop  32532  idunop  32589  elunop2  32624  fmptco1f1o  33278  padct  33361  mndlactf1o  33641  mndractf1o  33642  symgcom  33694  cycpmconjvlem  33752  cycpmconjslem2  33766  1arithidomlem2  34118  esplysply  34253  xrge0iifiso  34617  volmeas  34914  ballotlemro  35205  jf1o  35962  prconf1acwevd  35999  vonf1oonfo  36000  derangenlem  36054  subfacp1lem3  36065  subfacp1lem5  36067  erdsze2lem1  36086  cvmsss2  36157  poimirlem1  38676  poimirlem2  38677  poimirlem3  38678  poimirlem4  38679  poimirlem5  38680  poimirlem6  38681  poimirlem7  38682  poimirlem9  38684  poimirlem10  38685  poimirlem11  38686  poimirlem12  38687  poimirlem14  38689  poimirlem15  38690  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem22  38697  poimirlem23  38698  poimirlem24  38699  poimirlem25  38700  poimirlem29  38704  poimirlem31  38706  mblfinlem2  38713  ismtybndlem  38877  ismtyres  38879  diaintclN  42252  dibintclN  42361  mapdrn  42843  aks6d1c1p5  43299  riccrng1  43719  ricdrng1  43729  dnnumch2  44189  kelac1  44202  lnmlmic  44227  pwslnmlem1  44231  pwfi2f1o  44235  gicabl  44238  imasgim  44239  isnumbasgrplem1  44240  ntrneifv2  45217  stoweidlem27  47173  fourierdlem20  47273  fourierdlem51  47303  fourierdlem52  47304  fourierdlem63  47315  fourierdlem64  47316  fourierdlem65  47317  fourierdlem102  47354  fourierdlem114  47366  sge0f1o  47528  nnfoctbdjlem  47601  isomenndlem  47676  ovnsubaddlem1  47716  3f1oss1  48281  f1oresf1o2  48497  grimuhgr  49121  grimcnv  49122  isuspgrimlem  49129  grimedg  49169  isubgr3stgrlem8  49207  tposres3  50130  uptrlem1  50462  lmdran  50990  cmdlan  50991