Theorem f1f1orn 6814

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 6760	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6519	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6813	. 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 5640  ran crn 5642  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  –1-1→wf1 6511  –1-1-onto→wf1o 6513

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1ores  6817  f1un  6823  f1cnv  6827  f1cocnv1  6833  f1ocnvfvrneq  7264  fnwelem  8113  oacomf1olem  8531  sucdom2OLD  9056  domss2  9106  ssenen  9121  sucdom2  9173  f1finf1o  9223  f1finf1oOLD  9224  infn0  9258  f1fi  9270  f1dmvrnfibi  9299  marypha1lem  9391  hartogslem1  9502  infdifsn  9617  infxpenlem  9973  infxpenc2lem1  9979  fseqenlem2  9985  ac10ct  9994  acndom  10011  acndom2  10014  dfac12lem2  10105  dfac12lem3  10106  fictb  10204  fin23lem21  10299  axcc2lem  10396  pwfseqlem1  10618  pwfseqlem5  10623  hashf1lem1  14427  hashf1lem2  14428  4sqlem11  16933  xpsff1o2  17539  yoniso  18253  imasmndf1  18710  imasgrpf1  18996  conjsubgen  19190  ghmqusker  19226  cayley  19351  odinf  19500  sylow1lem2  19536  sylow2blem1  19557  gsumval3lem2  19843  gsumval3  19844  dprdf1  19972  imasrngf1  20094  imasringf1  20247  islindf3  21742  uvcf1o  21762  2ndcdisj  23350  dis2ndc  23354  qtopf1  23710  ovolicc2lem4  25428  itg1addlem4  25607  basellem3  27000  fsumvma  27131  dchrisum0fno1  27429  usgrf1o  29105  uspgrf1oedg  29107  usgrf1oedg  29141  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  fnpreimac  32602  fsumiunle  32761  cshf1o  32891  tocycfvres1  33074  tocycfvres2  33075  cycpmfv1  33077  cycpmfv2  33078  cycpmcl  33080  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  tocyccntz  33108  cycpmconjslem1  33118  cycpmconjslem2  33119  idomsubr  33266  dimkerim  33630  esumiun  34091  onvf1od  35101  erdszelem10  35194  mrsubff1o  35509  msubff1o  35551  f1omptsnlem  37331  pibt2  37412  matunitlindflem2  37618  dihcnvcl  41272  dihcnvid1  41273  dihcnvid2  41274  dihlspsnat  41334  dihglblem6  41341  dochocss  41367  dochnoncon  41392  mapdcnvcl  41653  mapdcnvid2  41658  eldioph2lem2  42756  dnwech  43044  cantnfub  43317  disjf1o  45192  f1ocof1ob2  47087  gricushgr  47921  ushggricedg  47931  imaf1homlem  49100  aacllem  49794