Theorem f1f1orn 6774

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 6720	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6486	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6773	. 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 5613  ran crn 5615  Fun wfun 6475   Fn wfn 6476  ⟶wf 6477  –1-1→wf1 6478  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1ores  6777  f1un  6783  f1cnv  6787  f1cocnv1  6793  f1ocnvfvrneq  7220  fnwelem  8061  oacomf1olem  8479  domss2  9049  ssenen  9064  sucdom2  9112  f1finf1o  9157  infn0  9186  f1fi  9198  f1dmvrnfibi  9225  marypha1lem  9317  hartogslem1  9428  infdifsn  9547  infxpenlem  9904  infxpenc2lem1  9910  fseqenlem2  9916  ac10ct  9925  acndom  9942  acndom2  9945  dfac12lem2  10036  dfac12lem3  10037  fictb  10135  fin23lem21  10230  axcc2lem  10327  pwfseqlem1  10549  pwfseqlem5  10554  hashf1lem1  14362  hashf1lem2  14363  4sqlem11  16867  xpsff1o2  17473  yoniso  18191  imasmndf1  18684  imasgrpf1  18970  conjsubgen  19163  ghmqusker  19199  cayley  19326  odinf  19475  sylow1lem2  19511  sylow2blem1  19532  gsumval3lem2  19818  gsumval3  19819  dprdf1  19947  imasrngf1  20096  imasringf1  20249  islindf3  21763  uvcf1o  21783  2ndcdisj  23371  dis2ndc  23375  qtopf1  23731  ovolicc2lem4  25448  itg1addlem4  25627  basellem3  27020  fsumvma  27151  dchrisum0fno1  27449  usgrf1o  29149  uspgrf1oedg  29151  usgrf1oedg  29185  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  fnpreimac  32653  fsumiunle  32812  cshf1o  32943  tocycfvres1  33079  tocycfvres2  33080  cycpmfv1  33082  cycpmfv2  33083  cycpmcl  33085  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  tocyccntz  33113  cycpmconjslem1  33123  cycpmconjslem2  33124  idomsubr  33275  dimkerim  33640  esumiun  34107  onvf1od  35151  erdszelem10  35244  mrsubff1o  35559  msubff1o  35601  f1omptsnlem  37380  pibt2  37461  matunitlindflem2  37656  dihcnvcl  41369  dihcnvid1  41370  dihcnvid2  41371  dihlspsnat  41431  dihglblem6  41438  dochocss  41464  dochnoncon  41489  mapdcnvcl  41750  mapdcnvid2  41755  eldioph2lem2  42853  dnwech  43140  cantnfub  43413  disjf1o  45287  f1ocof1ob2  47181  gricushgr  48016  ushggricedg  48026  imaf1homlem  49207  aacllem  49901