Theorem f1f1orn 6843

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 6787	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6547	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 495	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6842	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 581	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549

This theorem is referenced by:  f1ores  6846  f1un  6852  f1cnv  6856  f1cocnv1  6862  f1ocnvfvrneq  7286  fnwelem  8119  oacomf1olem  8566  sucdom2OLD  9084  domss2  9138  ssenen  9153  sucdom2  9208  f1finf1o  9273  f1finf1oOLD  9274  infn0  9309  f1dmvrnfibi  9338  f1fi  9341  marypha1lem  9430  hartogslem1  9539  infdifsn  9654  infxpenlem  10010  infxpenc2lem1  10016  fseqenlem2  10022  ac10ct  10031  acndom  10048  acndom2  10051  dfac12lem2  10141  dfac12lem3  10142  fictb  10242  fin23lem21  10336  axcc2lem  10433  pwfseqlem1  10655  pwfseqlem5  10660  hashf1lem1  14419  hashf1lem1OLD  14420  hashf1lem2  14421  4sqlem11  16892  xpsff1o2  17519  yoniso  18242  imasmndf1  18698  imasgrpf1  18976  conjsubgen  19165  cayley  19323  odinf  19472  sylow1lem2  19508  sylow2blem1  19529  gsumval3lem2  19815  gsumval3  19816  dprdf1  19944  imasrngf1  20072  imasringf1  20219  islindf3  21600  uvcf1o  21620  2ndcdisj  23180  dis2ndc  23184  qtopf1  23540  ovolicc2lem4  25269  itg1addlem4  25448  itg1addlem4OLD  25449  basellem3  26823  fsumvma  26952  dchrisum0fno1  27250  usgrf1o  28698  uspgrf1oedg  28700  usgrf1oedg  28731  clwlkclwwlklem2a4  29517  clwlkclwwlklem2a  29518  fnpreimac  32163  fsumiunle  32302  cshf1o  32393  tocycfvres1  32539  tocycfvres2  32540  cycpmfv1  32542  cycpmfv2  32543  cycpmcl  32545  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  tocyccntz  32573  cycpmconjslem1  32583  cycpmconjslem2  32584  ghmqusker  32806  dimkerim  33000  esumiun  33390  erdszelem10  34489  mrsubff1o  34804  msubff1o  34846  f1omptsnlem  36520  pibt2  36601  matunitlindflem2  36788  dihcnvcl  40445  dihcnvid1  40446  dihcnvid2  40447  dihlspsnat  40507  dihglblem6  40514  dochocss  40540  dochnoncon  40565  mapdcnvcl  40826  mapdcnvid2  40831  eldioph2lem2  41801  dnwech  42092  cantnfub  42373  disjf1o  44188  f1ocof1ob2  46088  isomushgr  46792  ushrisomgr  46807  aacllem  47935