Theorem f1f1orn 6837

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 6780	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6546	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 503	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6836	. 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 5662  ran crn 5664  Fun wfun 6535   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538  –1-1-onto→wf1o 6540

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is used by:  f1ores  6840  f1un  6846  f1cnv  6850  f1cocnv1  6856  f1ocnvfvrneq  7294  f1we  7363  fnwelem  8134  oacomf1olem  8556  domss2  9132  ssenen  9147  sucdom2  9195  f1finf1o  9241  infn0  9270  f1fi  9282  f1dmvrnfibi  9306  marypha1lem  9401  hartogslem1  9512  infdifsn  9634  infxpenlem  10014  infxpenc2lem1  10020  fseqenlem2  10026  acndom  10052  acndom2  10055  dfac12lem2  10145  dfac12lem3  10146  fictb  10244  fin23lem21  10339  axcc2lem  10436  pwfseqlem1  10663  pwfseqlem5  10668  hashf1lem1  14515  hashf1lem2  14516  4sqlem11  17042  xpsff1o2  17650  yoniso  18368  imasmndf1  18876  imasgrpf1  19172  conjsubgen  19370  ghmqusker  19406  cayley  19533  odinf  19682  sylow1lem2  19718  sylow2blem1  19739  gsumval3lem2  20025  gsumval3  20026  dprdf1  20154  imasrngf1  20305  imasringf1  20464  islindf3  22031  uvcf1o  22051  2ndcdisj  23669  dis2ndc  23673  qtopf1  24029  ovolicc2lem4  25735  itg1addlem4  25914  basellem3  27303  fsumvma  27433  dchrisum0fno1  27731  usgrf1o  29584  uspgrf1oedg  29586  usgrf1oedg  29620  clwlkclwwlklem2a4  30420  clwlkclwwlklem2a  30421  fnpreimac  33091  fsumiunle  33248  cshf1o  33351  tocycfvres1  33499  tocycfvres2  33500  cycpmfv1  33502  cycpmfv2  33503  cycpmcl  33505  cycpmco2lem4  33518  cycpmco2lem5  33519  cycpmco2lem6  33520  cycpmco2lem7  33521  cycpmco2  33522  tocyccntz  33533  cycpmconjslem1  33543  cycpmconjslem2  33544  idomsubr  33699  dimkerim  34086  esumiun  34553  onvf1od  35653  erdszelem10  35734  mrsubff1o  36049  msubff1o  36091  f1omptsnlem  38044  pibt2  38125  matunitlindflem2  38330  dihcnvcl  42108  dihcnvid1  42109  dihcnvid2  42110  dihlspsnat  42170  dihglblem6  42177  dochocss  42203  dochnoncon  42228  mapdcnvcl  42489  mapdcnvid2  42494  eldioph2lem2  43570  cantnfub  44126  disjf1o  45987  f1ocof1ob2  47897  gricushgr  48760  ushggricedg  48770  imaf1homlem  49962  aacllem  50698