Theorem f1f1orn 6711

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

Syntax hints:   → wi 4  ^◡ccnv 5579  ran crn 5581  Fun wfun 6412   Fn wfn 6413  ⟶wf 6414  –1-1→wf1 6415  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1ores  6714  f1cnv  6723  f1cocnv1  6729  f1ocnvfvrneq  7138  fnwelem  7943  oacomf1olem  8357  sucdom2  8822  domss2  8872  ssenen  8887  f1finf1o  8975  f1dmvrnfibi  9033  f1fi  9036  marypha1lem  9122  hartogslem1  9231  infdifsn  9345  infxpenlem  9700  infxpenc2lem1  9706  fseqenlem2  9712  ac10ct  9721  acndom  9738  acndom2  9741  dfac12lem2  9831  dfac12lem3  9832  fictb  9932  fin23lem21  10026  axcc2lem  10123  pwfseqlem1  10345  pwfseqlem5  10350  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  4sqlem11  16584  xpsff1o2  17197  yoniso  17919  imasmndf1  18339  imasgrpf1  18607  conjsubgen  18782  cayley  18937  odinf  19085  sylow1lem2  19119  sylow2blem1  19140  gsumval3lem2  19422  gsumval3  19423  dprdf1  19551  islindf3  20943  uvcf1o  20963  2ndcdisj  22515  dis2ndc  22519  qtopf1  22875  ovolicc2lem4  24589  itg1addlem4  24768  itg1addlem4OLD  24769  basellem3  26137  fsumvma  26266  dchrisum0fno1  26564  usgrf1o  27444  uspgrf1oedg  27446  usgrf1oedg  27477  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  fnpreimac  30910  fsumiunle  31045  cshf1o  31136  tocycfvres1  31279  tocycfvres2  31280  cycpmfv1  31282  cycpmfv2  31283  cycpmcl  31285  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  tocyccntz  31313  cycpmconjslem1  31323  cycpmconjslem2  31324  dimkerim  31610  esumiun  31962  erdszelem10  33062  mrsubff1o  33377  msubff1o  33419  f1omptsnlem  35434  pibt2  35515  matunitlindflem2  35701  dihcnvcl  39212  dihcnvid1  39213  dihcnvid2  39214  dihlspsnat  39274  dihglblem6  39281  dochocss  39307  dochnoncon  39332  mapdcnvcl  39593  mapdcnvid2  39598  eldioph2lem2  40499  dnwech  40789  disjf1o  42618  f1ocof1ob2  44461  isomushgr  45166  ushrisomgr  45181  aacllem  46391