Theorem f1f1orn 6727

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 6671	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6438	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6726	. 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 5588  ran crn 5590  Fun wfun 6427   Fn wfn 6428  ⟶wf 6429  –1-1→wf1 6430  –1-1-onto→wf1o 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440

This theorem is referenced by:  f1ores  6730  f1un  6736  f1cnv  6740  f1cocnv1  6746  f1ocnvfvrneq  7158  fnwelem  7972  oacomf1olem  8395  sucdom2OLD  8869  domss2  8923  ssenen  8938  sucdom2  8989  f1finf1o  9046  f1dmvrnfibi  9103  f1fi  9106  marypha1lem  9192  hartogslem1  9301  infdifsn  9415  infxpenlem  9769  infxpenc2lem1  9775  fseqenlem2  9781  ac10ct  9790  acndom  9807  acndom2  9810  dfac12lem2  9900  dfac12lem3  9901  fictb  10001  fin23lem21  10095  axcc2lem  10192  pwfseqlem1  10414  pwfseqlem5  10419  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1lem2  14170  4sqlem11  16656  xpsff1o2  17280  yoniso  18003  imasmndf1  18424  imasgrpf1  18692  conjsubgen  18867  cayley  19022  odinf  19170  sylow1lem2  19204  sylow2blem1  19225  gsumval3lem2  19507  gsumval3  19508  dprdf1  19636  islindf3  21033  uvcf1o  21053  2ndcdisj  22607  dis2ndc  22611  qtopf1  22967  ovolicc2lem4  24684  itg1addlem4  24863  itg1addlem4OLD  24864  basellem3  26232  fsumvma  26361  dchrisum0fno1  26659  usgrf1o  27541  uspgrf1oedg  27543  usgrf1oedg  27574  clwlkclwwlklem2a4  28361  clwlkclwwlklem2a  28362  fnpreimac  31008  fsumiunle  31143  cshf1o  31234  tocycfvres1  31377  tocycfvres2  31378  cycpmfv1  31380  cycpmfv2  31381  cycpmcl  31383  cycpmco2lem4  31396  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2lem7  31399  cycpmco2  31400  tocyccntz  31411  cycpmconjslem1  31421  cycpmconjslem2  31422  dimkerim  31708  esumiun  32062  erdszelem10  33162  mrsubff1o  33477  msubff1o  33519  f1omptsnlem  35507  pibt2  35588  matunitlindflem2  35774  dihcnvcl  39285  dihcnvid1  39286  dihcnvid2  39287  dihlspsnat  39347  dihglblem6  39354  dochocss  39380  dochnoncon  39405  mapdcnvcl  39666  mapdcnvid2  39671  eldioph2lem2  40583  dnwech  40873  disjf1o  42729  f1ocof1ob2  44574  isomushgr  45278  ushrisomgr  45293  aacllem  46505