Theorem f1f1orn 6795

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 6741	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6507	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6794	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 584	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5633  ran crn 5635  Fun wfun 6496   Fn wfn 6497  ⟶wf 6498  –1-1→wf1 6499  –1-1-onto→wf1o 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509

This theorem is referenced by:  f1ores  6798  f1un  6804  f1cnv  6808  f1cocnv1  6814  f1ocnvfvrneq  7244  fnwelem  8085  oacomf1olem  8503  domss2  9078  ssenen  9093  sucdom2  9141  f1finf1o  9187  infn0  9216  f1fi  9228  f1dmvrnfibi  9255  marypha1lem  9350  hartogslem1  9461  infdifsn  9580  infxpenlem  9937  infxpenc2lem1  9943  fseqenlem2  9949  ac10ct  9958  acndom  9975  acndom2  9978  dfac12lem2  10069  dfac12lem3  10070  fictb  10168  fin23lem21  10263  axcc2lem  10360  pwfseqlem1  10583  pwfseqlem5  10588  hashf1lem1  14392  hashf1lem2  14393  4sqlem11  16897  xpsff1o2  17504  yoniso  18222  imasmndf1  18715  imasgrpf1  19004  conjsubgen  19197  ghmqusker  19233  cayley  19360  odinf  19509  sylow1lem2  19545  sylow2blem1  19566  gsumval3lem2  19852  gsumval3  19853  dprdf1  19981  imasrngf1  20130  imasringf1  20284  islindf3  21798  uvcf1o  21818  2ndcdisj  23417  dis2ndc  23421  qtopf1  23777  ovolicc2lem4  25494  itg1addlem4  25673  basellem3  27066  fsumvma  27197  dchrisum0fno1  27495  usgrf1o  29262  uspgrf1oedg  29264  usgrf1oedg  29298  clwlkclwwlklem2a4  30090  clwlkclwwlklem2a  30091  fnpreimac  32766  fsumiunle  32927  cshf1o  33061  tocycfvres1  33210  tocycfvres2  33211  cycpmfv1  33213  cycpmfv2  33214  cycpmcl  33216  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem6  33231  cycpmco2lem7  33232  cycpmco2  33233  tocyccntz  33244  cycpmconjslem1  33254  cycpmconjslem2  33255  idomsubr  33409  dimkerim  33811  esumiun  34278  onvf1od  35329  erdszelem10  35422  mrsubff1o  35737  msubff1o  35779  f1omptsnlem  37618  pibt2  37699  matunitlindflem2  37897  dihcnvcl  41676  dihcnvid1  41677  dihcnvid2  41678  dihlspsnat  41738  dihglblem6  41745  dochocss  41771  dochnoncon  41796  mapdcnvcl  42057  mapdcnvid2  42062  eldioph2lem2  43147  dnwech  43434  cantnfub  43707  disjf1o  45579  f1ocof1ob2  47471  gricushgr  48306  ushggricedg  48316  imaf1homlem  49495  aacllem  50189