Theorem f1f1orn 6793

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 6739	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6504	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6792	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 583	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5630  ran crn 5632  Fun wfun 6493   Fn wfn 6494  ⟶wf 6495  –1-1→wf1 6496  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1ores  6796  f1un  6802  f1cnv  6806  f1cocnv1  6812  f1ocnvfvrneq  7243  fnwelem  8087  oacomf1olem  8505  domss2  9077  ssenen  9092  sucdom2  9144  f1finf1o  9192  f1finf1oOLD  9193  infn0  9227  f1fi  9239  f1dmvrnfibi  9268  marypha1lem  9360  hartogslem1  9471  infdifsn  9586  infxpenlem  9942  infxpenc2lem1  9948  fseqenlem2  9954  ac10ct  9963  acndom  9980  acndom2  9983  dfac12lem2  10074  dfac12lem3  10075  fictb  10173  fin23lem21  10268  axcc2lem  10365  pwfseqlem1  10587  pwfseqlem5  10592  hashf1lem1  14396  hashf1lem2  14397  4sqlem11  16902  xpsff1o2  17508  yoniso  18226  imasmndf1  18685  imasgrpf1  18971  conjsubgen  19165  ghmqusker  19201  cayley  19328  odinf  19477  sylow1lem2  19513  sylow2blem1  19534  gsumval3lem2  19820  gsumval3  19821  dprdf1  19949  imasrngf1  20098  imasringf1  20251  islindf3  21768  uvcf1o  21788  2ndcdisj  23376  dis2ndc  23380  qtopf1  23736  ovolicc2lem4  25454  itg1addlem4  25633  basellem3  27026  fsumvma  27157  dchrisum0fno1  27455  usgrf1o  29151  uspgrf1oedg  29153  usgrf1oedg  29187  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  fnpreimac  32645  fsumiunle  32804  cshf1o  32934  tocycfvres1  33082  tocycfvres2  33083  cycpmfv1  33085  cycpmfv2  33086  cycpmcl  33088  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2lem7  33104  cycpmco2  33105  tocyccntz  33116  cycpmconjslem1  33126  cycpmconjslem2  33127  idomsubr  33275  dimkerim  33616  esumiun  34077  onvf1od  35087  erdszelem10  35180  mrsubff1o  35495  msubff1o  35537  f1omptsnlem  37317  pibt2  37398  matunitlindflem2  37604  dihcnvcl  41258  dihcnvid1  41259  dihcnvid2  41260  dihlspsnat  41320  dihglblem6  41327  dochocss  41353  dochnoncon  41378  mapdcnvcl  41639  mapdcnvid2  41644  eldioph2lem2  42742  dnwech  43030  cantnfub  43303  disjf1o  45178  f1ocof1ob2  47076  gricushgr  47910  ushggricedg  47920  imaf1homlem  49089  aacllem  49783