Theorem f1f1orn 6832

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 6775	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6540	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 503	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6831	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 595	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5654  ran crn 5656  Fun wfun 6529   Fn wfn 6530  ⟶wf 6531  –1-1→wf1 6532  –1-1-onto→wf1o 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2752  df-ss 3916  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542

This theorem is used by:  f1ores  6835  f1un  6841  f1cnv  6845  f1cocnv1  6851  f1ocnvfvrneq  7290  f1we  7359  fnwelem  8134  oacomf1olem  8558  domss2  9141  ssenen  9156  sucdom2  9204  f1finf1o  9250  infn0  9279  f1fi  9291  f1dmvrnfibi  9315  marypha1lem  9410  hartogslem1  9521  infdifsn  9643  infxpenlem  10041  infxpenc2lem1  10047  fseqenlem2  10053  acndom  10079  acndom2  10082  dfac12lem2  10172  dfac12lem3  10173  fictb  10271  fin23lem21  10366  axcc2lem  10463  pwfseqlem1  10692  pwfseqlem5  10697  hashf1lem1  14545  hashf1lem2  14546  4sqlem11  17072  xpsff1o2  17680  yoniso  18398  imasmndf1  18909  imasgrpf1  19206  conjsubgen  19404  ghmqusker  19440  cayley  19567  odinf  19716  sylow1lem2  19752  sylow2blem1  19773  gsumval3lem2  20059  gsumval3  20060  dprdf1  20188  imasrngf1  20339  imasringf1  20500  islindf3  22071  uvcf1o  22091  matunitlindflem2  22934  2ndcdisj  23714  dis2ndc  23718  qtopf1  24074  ovolicc2lem4  25780  itg1addlem4  25959  basellem3  27351  fsumvma  27481  dchrisum0fno1  27779  usgrf1o  29663  uspgrf1oedg  29665  usgrf1oedg  29699  clwlkclwwlklem2a4  30499  clwlkclwwlklem2a  30500  fnpreimac  33175  fsumiunle  33331  cshf1o  33434  tocycfvres1  33582  tocycfvres2  33583  cycpmfv1  33585  cycpmfv2  33586  cycpmcl  33588  cycpmco2lem4  33601  cycpmco2lem5  33602  cycpmco2lem6  33603  cycpmco2lem7  33604  cycpmco2  33605  tocyccntz  33616  cycpmconjslem1  33626  cycpmconjslem2  33627  idomsubr  33782  dimkerim  34170  esumiun  34637  onvf1od  35787  erdszelem10  35862  mrsubff1o  36177  msubff1o  36219  f1omptsnlem  38155  pibt2  38236  dihcnvcl  42209  dihcnvid1  42210  dihcnvid2  42211  dihlspsnat  42271  dihglblem6  42278  dochocss  42304  dochnoncon  42329  mapdcnvcl  42590  mapdcnvid2  42595  eldioph2lem2  43671  cantnfub  44227  disjf1o  46088  f1ocof1ob2  48035  gricushgr  48898  ushggricedg  48908  imaf1homlem  50098  aacllem  50837