Theorem f1f1orn 6613

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 6561	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6340	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 500	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6612	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 586	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5523  ran crn 5525  Fun wfun 6329   Fn wfn 6330  ⟶wf 6331  –1-1→wf1 6332  –1-1-onto→wf1o 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342

This theorem is referenced by:  f1ores  6616  f1cnv  6625  f1cocnv1  6631  f1ocnvfvrneq  7034  fnwelem  7830  oacomf1olem  8200  sucdom2  8648  domss2  8698  ssenen  8713  f1finf1o  8782  f1dmvrnfibi  8841  f1fi  8844  marypha1lem  8930  hartogslem1  9039  infdifsn  9153  infxpenlem  9473  infxpenc2lem1  9479  fseqenlem2  9485  ac10ct  9494  acndom  9511  acndom2  9514  dfac12lem2  9604  dfac12lem3  9605  fictb  9705  fin23lem21  9799  axcc2lem  9896  pwfseqlem1  10118  pwfseqlem5  10123  hashf1lem1  13864  hashf1lem1OLD  13865  hashf1lem2  13866  4sqlem11  16346  xpsff1o2  16900  yoniso  17601  imasmndf1  18016  imasgrpf1  18283  conjsubgen  18458  cayley  18609  odinf  18757  sylow1lem2  18791  sylow2blem1  18812  gsumval3lem2  19094  gsumval3  19095  dprdf1  19223  islindf3  20591  uvcf1o  20611  2ndcdisj  22156  dis2ndc  22160  qtopf1  22516  ovolicc2lem4  24220  itg1addlem4  24399  basellem3  25767  fsumvma  25896  dchrisum0fno1  26194  usgrf1o  27063  uspgrf1oedg  27065  usgrf1oedg  27096  clwlkclwwlklem2a4  27881  clwlkclwwlklem2a  27882  fnpreimac  30532  fsumiunle  30667  cshf1o  30758  tocycfvres1  30903  tocycfvres2  30904  cycpmfv1  30906  cycpmfv2  30907  cycpmcl  30909  cycpmco2lem4  30922  cycpmco2lem5  30923  cycpmco2lem6  30924  cycpmco2lem7  30925  cycpmco2  30926  tocyccntz  30937  cycpmconjslem1  30947  cycpmconjslem2  30948  dimkerim  31229  esumiun  31581  erdszelem10  32678  mrsubff1o  32993  msubff1o  33035  f1omptsnlem  35033  pibt2  35114  matunitlindflem2  35334  dihcnvcl  38847  dihcnvid1  38848  dihcnvid2  38849  dihlspsnat  38909  dihglblem6  38916  dochocss  38942  dochnoncon  38967  mapdcnvcl  39228  mapdcnvid2  39233  eldioph2lem2  40075  dnwech  40365  disjf1o  42188  isomushgr  44711  ushrisomgr  44726  aacllem  45720