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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5660  ran crn 5662  Fun wfun 6530   Fn wfn 6531  ⟶wf 6532  –1-1→wf1 6533  –1-1-onto→wf1o 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-cleq 2755  df-ss 3922  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is used by:  f1ores  6835  f1un  6841  f1cnv  6845  f1cocnv1  6851  f1ocnvfvrneq  7284  fnwelem  8123  oacomf1olem  8545  domss2  9120  ssenen  9135  sucdom2  9183  f1finf1o  9229  infn0  9258  f1fi  9270  f1dmvrnfibi  9294  marypha1lem  9389  hartogslem1  9500  infdifsn  9622  infxpenlem  10002  infxpenc2lem1  10008  fseqenlem2  10014  ac10ct  10023  acndom  10040  acndom2  10043  dfac12lem2  10133  dfac12lem3  10134  fictb  10232  fin23lem21  10327  axcc2lem  10424  pwfseqlem1  10647  pwfseqlem5  10652  hashf1lem1  14497  hashf1lem2  14498  4sqlem11  17019  xpsff1o2  17627  yoniso  18345  imasmndf1  18838  imasgrpf1  19127  conjsubgen  19325  ghmqusker  19361  cayley  19488  odinf  19637  sylow1lem2  19673  sylow2blem1  19694  gsumval3lem2  19980  gsumval3  19981  dprdf1  20109  imasrngf1  20260  imasringf1  20418  islindf3  21985  uvcf1o  22005  2ndcdisj  23622  dis2ndc  23626  qtopf1  23982  ovolicc2lem4  25688  itg1addlem4  25867  basellem3  27256  fsumvma  27386  dchrisum0fno1  27684  usgrf1o  29530  uspgrf1oedg  29532  usgrf1oedg  29566  clwlkclwwlklem2a4  30357  clwlkclwwlklem2a  30358  fnpreimac  33024  fsumiunle  33182  cshf1o  33291  tocycfvres1  33439  tocycfvres2  33440  cycpmfv1  33442  cycpmfv2  33443  cycpmcl  33445  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2lem7  33461  cycpmco2  33462  tocyccntz  33473  cycpmconjslem1  33483  cycpmconjslem2  33484  idomsubr  33639  dimkerim  34026  esumiun  34493  onvf1od  35599  erdszelem10  35700  mrsubff1o  36015  msubff1o  36057  f1omptsnlem  38010  pibt2  38091  matunitlindflem2  38296  dihcnvcl  42073  dihcnvid1  42074  dihcnvid2  42075  dihlspsnat  42135  dihglblem6  42142  dochocss  42168  dochnoncon  42193  mapdcnvcl  42454  mapdcnvid2  42459  eldioph2lem2  43520  dnwech  43803  cantnfub  44076  disjf1o  45937  f1ocof1ob2  47847  gricushgr  48710  ushggricedg  48720  imaf1homlem  49913  aacllem  50649