Theorem f1ofo 6789

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

Syntax hints:   → wi 4  ^◡ccnv 5631  Fun wfun 6494  –onto→wfo 6498  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1imacnv  6798  resin  6804  f1ococnv2  6809  fo00  6818  f1ounsn  7228  f1ocoima  7259  isoini  7294  isofrlem  7296  isoselem  7297  ncanth  7323  f1opw2  7623  f1dmex  7911  f1ovv  7912  f1oweALT  7926  wemoiso2  7928  mptcnfimad  7940  curry1  8056  curry2  8059  smoiso2  8311  f1osetex  8808  bren  8905  f1oeng  8919  en1  8973  canth2  9070  domss2  9076  mapen  9081  ssenen  9091  dif1enlem  9096  ssfiALT  9110  phplem2  9141  php3  9145  f1fi  9226  domunfican  9234  fiint  9239  f1opwfi  9268  mapfien  9323  supisolem  9389  ordiso2  9432  ordtypelem10  9444  oismo  9457  wdomref  9489  brwdom2  9490  unxpwdom2  9505  cantnflt2  9594  cantnfp1lem3  9601  wemapwe  9618  infxpenc2lem1  9941  fseqen  9949  infpwfien  9984  infmap2  10139  ackbij2  10164  cff1  10180  cofsmo  10191  infpssr  10230  enfin2i  10243  fin23lem27  10250  enfin1ai  10306  fin1a2lem7  10328  axcclem  10379  ttukeylem1  10431  fpwwe2lem5  10558  fpwwe2lem8  10561  canthp1lem2  10576  tskuni  10706  gruen  10735  cnexALT  12911  fiinfnf1o  14285  hasheqf1oi  14286  hashfacen  14389  fsumf1o  15658  fsumss  15660  fprodf1o  15881  fprodss  15883  ruc  16180  unbenlem  16848  xpsfrn  17501  xpsbas  17505  xpsadd  17507  xpsmul  17508  xpssca  17509  xpsvsca  17510  xpsless  17511  xpsle  17512  imasmndf1  18713  sursubmefmnd  18833  imasgrpf1  18999  gicsubgen  19220  symgmov2  19329  symgextfo  19363  symgfixelsi  19376  giccyg  19841  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  dprdf1o  19975  imasrngf1  20125  imasringf1  20279  gsumfsum  21401  znleval  21521  lmimlbs  21803  lbslcic  21808  coe1mul2lem2  22222  cmpfi  23364  idqtop  23662  basqtop  23667  tgqtop  23668  hmeontr  23725  hmeoimaf1o  23726  hmeoqtop  23731  cmphmph  23744  connhmph  23745  nrmhmph  23750  indishmph  23754  cmphaushmeo  23756  xpstps  23766  xpstopnlem2  23767  fmid  23916  tsmsf1o  24101  imasdsf1olem  24329  imasf1oxmet  24331  imasf1omet  24332  xpsdsfn  24333  imasf1oxms  24445  imasf1oms  24446  iccpnfhmeo  24911  cnheiborlem  24921  ovolctb  25459  ovolicc2lem4  25489  dyadmbl  25569  mbfimaopnlem  25624  itg1addlem4  25668  dvcnvrelem2  25991  dvcnvre  25992  deg1ldg  26065  deg1leb  26068  efifo  26524  logrn  26535  dvrelog  26614  efopnlem2  26634  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  f1otrg  28955  axcontlem10  29058  edgusgrnbfin  29458  eupthvdres  30322  cnvunop  32006  counop  32009  idunop  32066  elunop2  32101  fmptco1f1o  32723  padct  32808  mndlactf1o  33123  mndractf1o  33124  symgcom  33177  cycpmconjvlem  33235  cycpmconjslem2  33249  1arithidomlem2  33629  esplysply  33748  xrge0iifiso  34113  volmeas  34409  ballotlemro  34701  derangenlem  35387  subfacp1lem3  35398  subfacp1lem5  35400  erdsze2lem1  35419  cvmsss2  35490  poimirlem1  37872  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem9  37880  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem29  37900  poimirlem31  37902  mblfinlem2  37909  ismtybndlem  38057  ismtyres  38059  diaintclN  41434  dibintclN  41543  mapdrn  42025  aks6d1c1p5  42482  riccrng1  42891  ricdrng1  42898  dnnumch2  43402  kelac1  43420  lnmlmic  43445  pwslnmlem1  43449  pwfi2f1o  43453  gicabl  43456  imasgim  43457  isnumbasgrplem1  43458  ntrneifv2  44436  stoweidlem27  46385  fourierdlem20  46485  fourierdlem51  46515  fourierdlem52  46516  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem102  46566  fourierdlem114  46578  sge0f1o  46740  nnfoctbdjlem  46813  isomenndlem  46888  ovnsubaddlem1  46928  3f1oss1  47435  f1oresf1o2  47651  grimuhgr  48247  grimcnv  48248  isuspgrimlem  48255  grimedg  48295  isubgr3stgrlem8  48333  tposres3  49240  uptrlem1  49569  lmdran  50030  cmdlan  50031