Theorem f1ofo 6826

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 6825	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5654  Fun wfun 6527  –onto→wfo 6531  –1-1-onto→wf1o 6532

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2752  df-ss 3916  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1imacnv  6835  resin  6841  f1ococnv2  6846  fo00  6855  f1ounsn  7274  f1ocoima  7305  isoini  7340  isofrlem  7342  isoselem  7343  ncanth  7369  f1opw2  7670  f1dmex  7955  f1ovv  7956  f1oweALT  7970  wemoiso2  7972  mptcnfimad  7984  curry1  8102  curry2  8105  smoiso2  8359  f1osetex  8861  bren  8963  f1oeng  8977  en1  9031  canth2  9129  domss2  9135  mapen  9140  ssenen  9150  dif1enlem  9155  ssfiALT  9169  phplem2  9200  php3  9204  f1fi  9285  domunfican  9292  fiint  9297  f1opwfi  9324  mapfien  9379  supisolem  9445  ordiso2  9488  ordtypelem10  9500  oismo  9513  wdomref  9545  brwdom2  9546  unxpwdom2  9561  cantnflt2  9653  cantnfp1lem3  9660  wemapwe  9677  infxpenc2lem1  10023  fseqen  10031  infpwfien  10066  infmap2  10220  ackbij2  10245  cff1  10261  cofsmo  10272  infpssr  10311  enfin2i  10324  fin23lem27  10331  enfin1ai  10387  fin1a2lem7  10409  axcclem  10460  ttukeylem1  10512  fpwwe2lem5  10645  fpwwe2lem8  10648  canthp1lem2  10663  tskuni  10793  gruen  10822  cnexALT  13037  fiinfnf1o  14415  hasheqf1oi  14416  hashfacen  14520  fsumf1o  15810  fsumss  15812  fprodf1o  16034  fprodss  16036  ruc  16332  unbenlem  17001  xpsfrn  17655  xpsbas  17659  xpsadd  17661  xpsmul  17662  xpssca  17663  xpsvsca  17664  xpsless  17665  xpsle  17666  imasmndf1  18884  sursubmefmnd  19006  imasgrpf1  19181  gicsubgen  19407  symgmov2  19516  symgextfo  19550  symgfixelsi  19563  giccyg  20028  gsumzres  20037  gsumzcl2  20038  gsumzf1o  20040  gsumzaddlem  20049  gsumconst  20062  gsumzmhm  20065  gsumzoppg  20072  dprdf1o  20162  imasrngf1  20314  imasringf1  20473  gsumfsum  21648  znleval  21768  lmimlbs  22050  lbslcic  22055  coe1mul2lem2  22495  cmpfi  23634  idqtop  23933  basqtop  23938  tgqtop  23939  hmeontr  23996  hmeoimaf1o  23997  hmeoqtop  24002  cmphmph  24015  connhmph  24016  nrmhmph  24021  indishmph  24025  cmphaushmeo  24027  xpstps  24037  xpstopnlem2  24038  fmid  24187  tsmsf1o  24372  imasdsf1olem  24600  imasf1oxmet  24602  imasf1omet  24603  xpsdsfn  24604  imasf1oxms  24716  imasf1oms  24717  iccpnfhmeo  25174  cnheiborlem  25183  ovolctb  25719  ovolicc2lem4  25749  dyadmbl  25829  mbfimaopnlem  25884  itg1addlem4  25928  dvcnvrelem2  26246  dvcnvre  26247  deg1ldg  26318  deg1leb  26321  efifo  26785  logrn  26796  dvrelog  26875  efopnlem2  26895  fsumdvdsmul  27432  f1otrg  29328  axcontlem10  29431  edgusgrnbfin  29834  eupthvdres  30716  cnvunop  32400  counop  32403  idunop  32460  elunop2  32495  fmptco1f1o  33107  padct  33190  mndlactf1o  33471  mndractf1o  33472  symgcom  33524  cycpmconjvlem  33582  cycpmconjslem2  33596  1arithidomlem2  33947  esplysply  34082  xrge0iifiso  34446  volmeas  34743  ballotlemro  35035  vonf1oonfo  35713  derangenlem  35751  subfacp1lem3  35762  subfacp1lem5  35764  erdsze2lem1  35783  cvmsss2  35854  poimirlem1  38371  poimirlem2  38372  poimirlem3  38373  poimirlem4  38374  poimirlem5  38375  poimirlem6  38376  poimirlem7  38377  poimirlem9  38379  poimirlem10  38380  poimirlem11  38381  poimirlem12  38382  poimirlem14  38384  poimirlem15  38385  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem22  38392  poimirlem23  38393  poimirlem24  38394  poimirlem25  38395  poimirlem29  38399  poimirlem31  38401  mblfinlem2  38408  ismtybndlem  38557  ismtyres  38559  diaintclN  41932  dibintclN  42041  mapdrn  42523  aks6d1c1p5  42979  riccrng1  43404  ricdrng1  43411  dnnumch2  43887  kelac1  43905  lnmlmic  43930  pwslnmlem1  43934  pwfi2f1o  43938  gicabl  43941  imasgim  43942  isnumbasgrplem1  43943  ntrneifv2  44921  stoweidlem27  46856  fourierdlem20  46956  fourierdlem51  46986  fourierdlem52  46987  fourierdlem63  46998  fourierdlem64  46999  fourierdlem65  47000  fourierdlem102  47037  fourierdlem114  47049  sge0f1o  47211  nnfoctbdjlem  47284  isomenndlem  47359  ovnsubaddlem1  47399  3f1oss1  47964  f1oresf1o2  48180  grimuhgr  48804  grimcnv  48805  isuspgrimlem  48812  grimedg  48852  isubgr3stgrlem8  48890  tposres3  49808  uptrlem1  50137  lmdran  50598  cmdlan  50599