Theorem f1ofo 6832

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 6831	. 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 6532  –onto→wfo 6536  –1-1-onto→wf1o 6537

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is used by:  f1imacnv  6841  resin  6847  f1ococnv2  6852  fo00  6861  f1ounsn  7280  f1ocoima  7311  isoini  7346  isofrlem  7348  isoselem  7349  ncanth  7375  f1opw2  7676  f1dmex  7969  f1ovv  7970  f1oweALT  7984  wemoiso2  7986  mptcnfimad  7998  curry1  8115  curry2  8118  smoiso2  8377  f1osetex  8881  bren  8983  f1oeng  8997  en1  9051  canth2  9149  domss2  9155  mapen  9160  ssenen  9170  dif1enlem  9175  ssfiALT  9189  phplem2  9220  php3  9224  f1fi  9306  domunfican  9313  fiint  9318  f1opwfi  9345  mapfien  9400  supisolem  9466  ordiso2  9509  ordtypelem10  9521  oismo  9534  wdomref  9566  brwdom2  9567  unxpwdom2  9582  cantnflt2  9674  cantnfp1lem3  9681  wemapwe  9698  infxpenc2lem1  10098  fseqen  10106  infpwfien  10141  infmap2  10295  ackbij2  10320  cff1  10336  cofsmo  10347  infpssr  10386  enfin2i  10399  fin23lem27  10406  enfin1ai  10462  fin1a2lem7  10484  axcclem  10535  ttukeylem1  10587  fpwwe2lem5  10720  fpwwe2lem8  10723  canthp1lem2  10738  tskuni  10868  gruen  10897  cnexALT  13114  fiinfnf1o  14494  hasheqf1oi  14495  hashfacen  14599  fsumf1o  15889  fsumss  15891  fprodf1o  16113  fprodss  16115  ruc  16411  unbenlem  17086  xpsfrn  17740  xpsbas  17744  xpsadd  17746  xpsmul  17747  xpssca  17748  xpsvsca  17749  xpsless  17750  xpsle  17751  imasmndf1  18970  sursubmefmnd  19092  imasgrpf1  19267  gicsubgen  19493  symgmov2  19602  symgextfo  19636  symgfixelsi  19649  giccyg  20114  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  dprdf1o  20248  imasrngf1  20400  imasringf1  20561  gsumfsum  21740  znleval  21860  lmimlbs  22142  lbslcic  22147  coe1mul2lem2  22587  cmpfi  23726  idqtop  24025  basqtop  24030  tgqtop  24031  hmeontr  24088  hmeoimaf1o  24089  hmeoqtop  24094  cmphmph  24107  connhmph  24108  nrmhmph  24113  indishmph  24117  cmphaushmeo  24119  xpstps  24129  xpstopnlem2  24130  fmid  24279  tsmsf1o  24464  imasdsf1olem  24692  imasf1oxmet  24694  imasf1omet  24695  xpsdsfn  24696  imasf1oxms  24808  imasf1oms  24809  iccpnfhmeo  25266  cnheiborlem  25275  ovolctb  25811  ovolicc2lem4  25841  dyadmbl  25921  mbfimaopnlem  25976  itg1addlem4  26020  dvcnvrelem2  26338  dvcnvre  26339  deg1ldg  26410  deg1leb  26413  efifo  26875  logrn  26886  dvrelog  26965  efopnlem2  26985  fsumdvdsmul  27522  f1otrg  29448  axcontlem10  29551  edgusgrnbfin  29954  eupthvdres  30836  cnvunop  32520  counop  32523  idunop  32580  elunop2  32615  fmptco1f1o  33227  padct  33310  mndlactf1o  33591  mndractf1o  33592  symgcom  33644  cycpmconjvlem  33702  cycpmconjslem2  33716  1arithidomlem2  34068  esplysply  34203  xrge0iifiso  34567  volmeas  34864  ballotlemro  35155  vonf1oonfo  35898  derangenlem  35936  subfacp1lem3  35947  subfacp1lem5  35949  erdsze2lem1  35968  cvmsss2  36039  poimirlem1  38539  poimirlem2  38540  poimirlem3  38541  poimirlem4  38542  poimirlem5  38543  poimirlem6  38544  poimirlem7  38545  poimirlem9  38547  poimirlem10  38548  poimirlem11  38549  poimirlem12  38550  poimirlem14  38552  poimirlem15  38553  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem22  38560  poimirlem23  38561  poimirlem24  38562  poimirlem25  38563  poimirlem29  38567  poimirlem31  38569  mblfinlem2  38576  ismtybndlem  38740  ismtyres  38742  diaintclN  42115  dibintclN  42224  mapdrn  42706  aks6d1c1p5  43162  riccrng1  43582  ricdrng1  43592  dnnumch2  44051  kelac1  44064  lnmlmic  44089  pwslnmlem1  44093  pwfi2f1o  44097  gicabl  44100  imasgim  44101  isnumbasgrplem1  44102  ntrneifv2  45079  stoweidlem27  47036  fourierdlem20  47136  fourierdlem51  47166  fourierdlem52  47167  fourierdlem63  47178  fourierdlem64  47179  fourierdlem65  47180  fourierdlem102  47217  fourierdlem114  47229  sge0f1o  47391  nnfoctbdjlem  47464  isomenndlem  47539  ovnsubaddlem1  47579  3f1oss1  48144  f1oresf1o2  48360  grimuhgr  48984  grimcnv  48985  isuspgrimlem  48992  grimedg  49032  isubgr3stgrlem8  49070  tposres3  49988  uptrlem1  50317  lmdran  50778  cmdlan  50779