Theorem f1f1orn 6782

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 6728	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6494	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 499	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6781	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 590	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5620  ran crn 5622  Fun wfun 6483   Fn wfn 6484  ⟶wf 6485  –1-1→wf1 6486  –1-1-onto→wf1o 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-ex 1788  df-cleq 2733  df-ss 3902  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496

This theorem is referenced by:  f1ores  6785  f1un  6791  f1cnv  6795  f1cocnv1  6801  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  9573  infxpenlem  9930  infxpenc2lem1  9936  fseqenlem2  9942  ac10ct  9951  acndom  9968  acndom2  9971  dfac12lem2  10062  dfac12lem3  10063  fictb  10161  fin23lem21  10256  axcc2lem  10353  pwfseqlem1  10576  pwfseqlem5  10581  hashf1lem1  14412  hashf1lem2  14413  4sqlem11  16921  xpsff1o2  17528  yoniso  18246  imasmndf1  18739  imasgrpf1  19028  conjsubgen  19221  ghmqusker  19257  cayley  19384  odinf  19533  sylow1lem2  19569  sylow2blem1  19590  gsumval3lem2  19876  gsumval3  19877  dprdf1  20005  imasrngf1  20154  imasringf1  20306  islindf3  21805  uvcf1o  21825  2ndcdisj  23443  dis2ndc  23447  qtopf1  23803  ovolicc2lem4  25509  itg1addlem4  25688  basellem3  27068  fsumvma  27198  dchrisum0fno1  27496  usgrf1o  29262  uspgrf1oedg  29264  usgrf1oedg  29298  clwlkclwwlklem2a4  30089  clwlkclwwlklem2a  30090  fnpreimac  32766  fsumiunle  32925  cshf1o  33045  tocycfvres1  33195  tocycfvres2  33196  cycpmfv1  33198  cycpmfv2  33199  cycpmcl  33201  cycpmco2lem4  33214  cycpmco2lem5  33215  cycpmco2lem6  33216  cycpmco2lem7  33217  cycpmco2  33218  tocyccntz  33229  cycpmconjslem1  33239  cycpmconjslem2  33240  idomsubr  33397  dimkerim  33823  esumiun  34290  onvf1od  35350  erdszelem10  35443  mrsubff1o  35758  msubff1o  35800  f1omptsnlem  37713  pibt2  37794  matunitlindflem2  37999  dihcnvcl  41778  dihcnvid1  41779  dihcnvid2  41780  dihlspsnat  41840  dihglblem6  41847  dochocss  41873  dochnoncon  41898  mapdcnvcl  42159  mapdcnvid2  42164  eldioph2lem2  43225  dnwech  43508  cantnfub  43781  disjf1o  45652  f1ocof1ob2  47559  gricushgr  48422  ushggricedg  48432  imaf1homlem  49611  aacllem  50305