Theorem f1f1orn 6781

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 6727	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6493	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 499	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6780	. 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 5619  ran crn 5621  Fun wfun 6482   Fn wfn 6483  ⟶wf 6484  –1-1→wf1 6485  –1-1-onto→wf1o 6487

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 3901  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495

This theorem is referenced by:  f1ores  6784  f1un  6790  f1cnv  6794  f1cocnv1  6800  f1ocnvfvrneq  7233  fnwelem  8073  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  10257  axcc2lem  10354  pwfseqlem1  10577  pwfseqlem5  10582  hashf1lem1  14412  hashf1lem2  14413  4sqlem11  16921  xpsff1o2  17528  yoniso  18246  imasmndf1  18739  imasgrpf1  19028  conjsubgen  19220  ghmqusker  19256  cayley  19383  odinf  19532  sylow1lem2  19568  sylow2blem1  19589  gsumval3lem2  19875  gsumval3  19876  dprdf1  20004  imasrngf1  20153  imasringf1  20305  islindf3  21804  uvcf1o  21824  2ndcdisj  23442  dis2ndc  23446  qtopf1  23802  ovolicc2lem4  25508  itg1addlem4  25687  basellem3  27067  fsumvma  27197  dchrisum0fno1  27495  usgrf1o  29260  uspgrf1oedg  29262  usgrf1oedg  29296  clwlkclwwlklem2a4  30087  clwlkclwwlklem2a  30088  fnpreimac  32764  fsumiunle  32923  cshf1o  33043  tocycfvres1  33193  tocycfvres2  33194  cycpmfv1  33196  cycpmfv2  33197  cycpmcl  33199  cycpmco2lem4  33212  cycpmco2lem5  33213  cycpmco2lem6  33214  cycpmco2lem7  33215  cycpmco2  33216  tocyccntz  33227  cycpmconjslem1  33237  cycpmconjslem2  33238  idomsubr  33395  dimkerim  33821  esumiun  34288  onvf1od  35348  erdszelem10  35441  mrsubff1o  35756  msubff1o  35798  f1omptsnlem  37711  pibt2  37792  matunitlindflem2  37997  dihcnvcl  41776  dihcnvid1  41777  dihcnvid2  41778  dihlspsnat  41838  dihglblem6  41845  dochocss  41871  dochnoncon  41896  mapdcnvcl  42157  mapdcnvid2  42162  eldioph2lem2  43223  dnwech  43506  cantnfub  43779  disjf1o  45650  f1ocof1ob2  47557  gricushgr  48420  ushggricedg  48430  imaf1homlem  49609  aacllem  50303