Theorem f1f1orn 6786

Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)

Assertion

Ref	Expression
f1f1orn	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Proof of Theorem f1f1orn

Step	Hyp	Ref	Expression
1		f1fn 6732	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6498	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6785	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 584	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5624  ran crn 5626  Fun wfun 6487   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  –1-1-onto→wf1o 6492

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 3919  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  f1ores  6789  f1un  6795  f1cnv  6799  f1cocnv1  6805  f1ocnvfvrneq  7234  fnwelem  8075  oacomf1olem  8493  domss2  9068  ssenen  9083  sucdom2  9131  f1finf1o  9177  infn0  9206  f1fi  9218  f1dmvrnfibi  9245  marypha1lem  9340  hartogslem1  9451  infdifsn  9570  infxpenlem  9927  infxpenc2lem1  9933  fseqenlem2  9939  ac10ct  9948  acndom  9965  acndom2  9968  dfac12lem2  10059  dfac12lem3  10060  fictb  10158  fin23lem21  10253  axcc2lem  10350  pwfseqlem1  10573  pwfseqlem5  10578  hashf1lem1  14382  hashf1lem2  14383  4sqlem11  16887  xpsff1o2  17494  yoniso  18212  imasmndf1  18705  imasgrpf1  18991  conjsubgen  19184  ghmqusker  19220  cayley  19347  odinf  19496  sylow1lem2  19532  sylow2blem1  19553  gsumval3lem2  19839  gsumval3  19840  dprdf1  19968  imasrngf1  20117  imasringf1  20271  islindf3  21785  uvcf1o  21805  2ndcdisj  23404  dis2ndc  23408  qtopf1  23764  ovolicc2lem4  25481  itg1addlem4  25660  basellem3  27053  fsumvma  27184  dchrisum0fno1  27482  usgrf1o  29248  uspgrf1oedg  29250  usgrf1oedg  29284  clwlkclwwlklem2a4  30076  clwlkclwwlklem2a  30077  fnpreimac  32751  fsumiunle  32912  cshf1o  33046  tocycfvres1  33194  tocycfvres2  33195  cycpmfv1  33197  cycpmfv2  33198  cycpmcl  33200  cycpmco2lem4  33213  cycpmco2lem5  33214  cycpmco2lem6  33215  cycpmco2lem7  33216  cycpmco2  33217  tocyccntz  33228  cycpmconjslem1  33238  cycpmconjslem2  33239  idomsubr  33393  dimkerim  33786  esumiun  34253  onvf1od  35303  erdszelem10  35396  mrsubff1o  35711  msubff1o  35753  f1omptsnlem  37543  pibt2  37624  matunitlindflem2  37820  dihcnvcl  41599  dihcnvid1  41600  dihcnvid2  41601  dihlspsnat  41661  dihglblem6  41668  dochocss  41694  dochnoncon  41719  mapdcnvcl  41980  mapdcnvid2  41985  eldioph2lem2  43070  dnwech  43357  cantnfub  43630  disjf1o  45502  f1ocof1ob2  47395  gricushgr  48230  ushggricedg  48240  imaf1homlem  49419  aacllem  50113