Theorem f1f1orn 6859

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 6805	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6566	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6858	. 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 5684  ran crn 5686  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558  –1-1-onto→wf1o 6560

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1ores  6862  f1un  6868  f1cnv  6872  f1cocnv1  6878  f1ocnvfvrneq  7306  fnwelem  8156  oacomf1olem  8602  sucdom2OLD  9122  domss2  9176  ssenen  9191  sucdom2  9243  f1finf1o  9305  f1finf1oOLD  9306  infn0  9340  f1fi  9352  f1dmvrnfibi  9381  marypha1lem  9473  hartogslem1  9582  infdifsn  9697  infxpenlem  10053  infxpenc2lem1  10059  fseqenlem2  10065  ac10ct  10074  acndom  10091  acndom2  10094  dfac12lem2  10185  dfac12lem3  10186  fictb  10284  fin23lem21  10379  axcc2lem  10476  pwfseqlem1  10698  pwfseqlem5  10703  hashf1lem1  14494  hashf1lem2  14495  4sqlem11  16993  xpsff1o2  17614  yoniso  18330  imasmndf1  18789  imasgrpf1  19075  conjsubgen  19269  ghmqusker  19305  cayley  19432  odinf  19581  sylow1lem2  19617  sylow2blem1  19638  gsumval3lem2  19924  gsumval3  19925  dprdf1  20053  imasrngf1  20175  imasringf1  20328  islindf3  21846  uvcf1o  21866  2ndcdisj  23464  dis2ndc  23468  qtopf1  23824  ovolicc2lem4  25555  itg1addlem4  25734  basellem3  27126  fsumvma  27257  dchrisum0fno1  27555  usgrf1o  29188  uspgrf1oedg  29190  usgrf1oedg  29224  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  fnpreimac  32681  fsumiunle  32831  cshf1o  32947  tocycfvres1  33130  tocycfvres2  33131  cycpmfv1  33133  cycpmfv2  33134  cycpmcl  33136  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  tocyccntz  33164  cycpmconjslem1  33174  cycpmconjslem2  33175  idomsubr  33311  dimkerim  33678  esumiun  34095  erdszelem10  35205  mrsubff1o  35520  msubff1o  35562  f1omptsnlem  37337  pibt2  37418  matunitlindflem2  37624  dihcnvcl  41273  dihcnvid1  41274  dihcnvid2  41275  dihlspsnat  41335  dihglblem6  41342  dochocss  41368  dochnoncon  41393  mapdcnvcl  41654  mapdcnvid2  41659  eldioph2lem2  42772  dnwech  43060  cantnfub  43334  disjf1o  45196  f1ocof1ob2  47094  gricushgr  47886  ushggricedg  47896  aacllem  49320