Theorem f1f1orn 6836

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 6779	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6543	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 503	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6835	. 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 5649  ran crn 5651  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-cleq 2752  df-ss 3896  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is used by:  f1ores  6839  f1un  6845  f1cnv  6849  f1cocnv1  6855  f1ocnvfvrneq  7294  f1we  7363  fnwelem  8143  oacomf1olem  8572  domss2  9155  ssenen  9170  sucdom2  9218  f1finf1o  9264  infn0  9294  f1fi  9306  f1dmvrnfibi  9330  marypha1lem  9425  hartogslem1  9536  infdifsn  9658  infxpenlem  10092  infxpenc2lem1  10098  fseqenlem2  10104  acndom  10130  acndom2  10133  dfac12lem2  10223  dfac12lem3  10224  fictb  10322  fin23lem21  10417  axcc2lem  10514  pwfseqlem1  10743  pwfseqlem5  10748  hashf1lem1  14600  hashf1lem2  14601  4sqlem11  17133  xpsff1o2  17741  yoniso  18459  imasmndf1  18970  imasgrpf1  19267  conjsubgen  19465  ghmqusker  19501  cayley  19628  odinf  19777  sylow1lem2  19813  sylow2blem1  19834  gsumval3lem2  20120  gsumval3  20121  dprdf1  20249  imasrngf1  20400  imasringf1  20561  islindf3  22132  uvcf1o  22152  matunitlindflem2  22995  2ndcdisj  23775  dis2ndc  23779  qtopf1  24135  ovolicc2lem4  25841  itg1addlem4  26020  basellem3  27410  fsumvma  27540  dchrisum0fno1  27838  usgrf1o  29752  uspgrf1oedg  29754  usgrf1oedg  29788  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  fnpreimac  33264  fsumiunle  33420  cshf1o  33523  tocycfvres1  33671  tocycfvres2  33672  cycpmfv1  33674  cycpmfv2  33675  cycpmcl  33677  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  tocyccntz  33705  cycpmconjslem1  33715  cycpmconjslem2  33716  idomsubr  33871  dimkerim  34259  esumiun  34726  onvf1od  35886  onprcf1acwevd  35897  erdszelem10  35965  mrsubff1o  36280  msubff1o  36322  f1omptsnlem  38260  pibt2  38341  dihcnvcl  42329  dihcnvid1  42330  dihcnvid2  42331  dihlspsnat  42391  dihglblem6  42398  dochocss  42424  dochnoncon  42449  mapdcnvcl  42710  mapdcnvid2  42715  eldioph2lem2  43772  cantnfub  44323  disjf1o  46206  f1ocof1ob2  48152  gricushgr  49015  ushggricedg  49025  imaf1homlem  50215  aacllem  50939