Theorem f1f1orn 6833

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 6776	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6542	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 502	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6832	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 594	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5661  ran crn 5663  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  f1ores  6836  f1un  6842  f1cnv  6846  f1cocnv1  6852  f1ocnvfvrneq  7285  fnwelem  8127  oacomf1olem  8549  domss2  9124  ssenen  9139  sucdom2  9187  f1finf1o  9233  infn0  9262  f1fi  9274  f1dmvrnfibi  9298  marypha1lem  9393  hartogslem1  9504  infdifsn  9626  infxpenlem  9997  infxpenc2lem1  10003  fseqenlem2  10009  ac10ct  10018  acndom  10035  acndom2  10038  dfac12lem2  10128  dfac12lem3  10129  fictb  10227  fin23lem21  10323  axcc2lem  10420  pwfseqlem1  10643  pwfseqlem5  10648  hashf1lem1  14492  hashf1lem2  14493  4sqlem11  17015  xpsff1o2  17623  yoniso  18341  imasmndf1  18834  imasgrpf1  19123  conjsubgen  19321  ghmqusker  19357  cayley  19484  odinf  19633  sylow1lem2  19669  sylow2blem1  19690  gsumval3lem2  19976  gsumval3  19977  dprdf1  20105  imasrngf1  20256  imasringf1  20413  islindf3  21945  uvcf1o  21965  2ndcdisj  23582  dis2ndc  23586  qtopf1  23942  ovolicc2lem4  25648  itg1addlem4  25827  basellem3  27213  fsumvma  27343  dchrisum0fno1  27641  usgrf1o  29462  uspgrf1oedg  29464  usgrf1oedg  29498  clwlkclwwlklem2a4  30289  clwlkclwwlklem2a  30290  fnpreimac  32956  fsumiunle  33114  cshf1o  33223  tocycfvres1  33371  tocycfvres2  33372  cycpmfv1  33374  cycpmfv2  33375  cycpmcl  33377  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  tocyccntz  33405  cycpmconjslem1  33415  cycpmconjslem2  33416  idomsubr  33573  dimkerim  33962  esumiun  34429  onvf1od  35524  erdszelem10  35625  mrsubff1o  35940  msubff1o  35982  f1omptsnlem  37904  pibt2  37985  matunitlindflem2  38190  dihcnvcl  41969  dihcnvid1  41970  dihcnvid2  41971  dihlspsnat  42031  dihglblem6  42038  dochocss  42064  dochnoncon  42089  mapdcnvcl  42350  mapdcnvid2  42355  eldioph2lem2  43418  dnwech  43701  cantnfub  43974  disjf1o  45835  f1ocof1ob2  47742  gricushgr  48605  ushggricedg  48615  imaf1homlem  49804  aacllem  50509