Theorem f1f1orn 6775

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 6721	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6487	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6774	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 583	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5618  ran crn 5620  Fun wfun 6476   Fn wfn 6477  ⟶wf 6478  –1-1→wf1 6479  –1-1-onto→wf1o 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3920  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1ores  6778  f1un  6784  f1cnv  6788  f1cocnv1  6794  f1ocnvfvrneq  7223  fnwelem  8064  oacomf1olem  8482  domss2  9053  ssenen  9068  sucdom2  9117  f1finf1o  9162  infn0  9191  f1fi  9203  f1dmvrnfibi  9231  marypha1lem  9323  hartogslem1  9434  infdifsn  9553  infxpenlem  9907  infxpenc2lem1  9913  fseqenlem2  9919  ac10ct  9928  acndom  9945  acndom2  9948  dfac12lem2  10039  dfac12lem3  10040  fictb  10138  fin23lem21  10233  axcc2lem  10330  pwfseqlem1  10552  pwfseqlem5  10557  hashf1lem1  14362  hashf1lem2  14363  4sqlem11  16867  xpsff1o2  17473  yoniso  18191  imasmndf1  18650  imasgrpf1  18936  conjsubgen  19130  ghmqusker  19166  cayley  19293  odinf  19442  sylow1lem2  19478  sylow2blem1  19499  gsumval3lem2  19785  gsumval3  19786  dprdf1  19914  imasrngf1  20063  imasringf1  20216  islindf3  21733  uvcf1o  21753  2ndcdisj  23341  dis2ndc  23345  qtopf1  23701  ovolicc2lem4  25419  itg1addlem4  25598  basellem3  26991  fsumvma  27122  dchrisum0fno1  27420  usgrf1o  29116  uspgrf1oedg  29118  usgrf1oedg  29152  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  fnpreimac  32615  fsumiunle  32775  cshf1o  32905  tocycfvres1  33053  tocycfvres2  33054  cycpmfv1  33056  cycpmfv2  33057  cycpmcl  33059  cycpmco2lem4  33072  cycpmco2lem5  33073  cycpmco2lem6  33074  cycpmco2lem7  33075  cycpmco2  33076  tocyccntz  33087  cycpmconjslem1  33097  cycpmconjslem2  33098  idomsubr  33249  dimkerim  33600  esumiun  34067  onvf1od  35090  erdszelem10  35183  mrsubff1o  35498  msubff1o  35540  f1omptsnlem  37320  pibt2  37401  matunitlindflem2  37607  dihcnvcl  41260  dihcnvid1  41261  dihcnvid2  41262  dihlspsnat  41322  dihglblem6  41329  dochocss  41355  dochnoncon  41380  mapdcnvcl  41641  mapdcnvid2  41646  eldioph2lem2  42744  dnwech  43031  cantnfub  43304  disjf1o  45179  f1ocof1ob2  47076  gricushgr  47911  ushggricedg  47921  imaf1homlem  49102  aacllem  49796