Theorem f1f1orn 6845

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 6789	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6549	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 498	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6844	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 584	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5676  ran crn 5678  Fun wfun 6538   Fn wfn 6539  ⟶wf 6540  –1-1→wf1 6541  –1-1-onto→wf1o 6543

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1ores  6848  f1un  6854  f1cnv  6858  f1cocnv1  6864  f1ocnvfvrneq  7284  fnwelem  8117  oacomf1olem  8564  sucdom2OLD  9082  domss2  9136  ssenen  9151  sucdom2  9206  f1finf1o  9271  f1finf1oOLD  9272  infn0  9307  f1dmvrnfibi  9336  f1fi  9339  marypha1lem  9428  hartogslem1  9537  infdifsn  9652  infxpenlem  10008  infxpenc2lem1  10014  fseqenlem2  10020  ac10ct  10029  acndom  10046  acndom2  10049  dfac12lem2  10139  dfac12lem3  10140  fictb  10240  fin23lem21  10334  axcc2lem  10431  pwfseqlem1  10653  pwfseqlem5  10658  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  4sqlem11  16888  xpsff1o2  17515  yoniso  18238  imasmndf1  18664  imasgrpf1  18940  conjsubgen  19125  cayley  19282  odinf  19431  sylow1lem2  19467  sylow2blem1  19488  gsumval3lem2  19774  gsumval3  19775  dprdf1  19903  imasringf1  20144  islindf3  21381  uvcf1o  21401  2ndcdisj  22960  dis2ndc  22964  qtopf1  23320  ovolicc2lem4  25037  itg1addlem4  25216  itg1addlem4OLD  25217  basellem3  26587  fsumvma  26716  dchrisum0fno1  27014  usgrf1o  28431  uspgrf1oedg  28433  usgrf1oedg  28464  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  fnpreimac  31896  fsumiunle  32035  cshf1o  32126  tocycfvres1  32269  tocycfvres2  32270  cycpmfv1  32272  cycpmfv2  32273  cycpmcl  32275  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmco2  32292  tocyccntz  32303  cycpmconjslem1  32313  cycpmconjslem2  32314  ghmqusker  32532  dimkerim  32712  esumiun  33092  erdszelem10  34191  mrsubff1o  34506  msubff1o  34548  f1omptsnlem  36217  pibt2  36298  matunitlindflem2  36485  dihcnvcl  40142  dihcnvid1  40143  dihcnvid2  40144  dihlspsnat  40204  dihglblem6  40211  dochocss  40237  dochnoncon  40262  mapdcnvcl  40523  mapdcnvid2  40528  eldioph2lem2  41499  dnwech  41790  cantnfub  42071  disjf1o  43889  f1ocof1ob2  45790  isomushgr  46494  ushrisomgr  46509  imasrngf1  46679  aacllem  47848