Theorem f1f1orn 6811

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 6757	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6516	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6810	. 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 5637  ran crn 5639  Fun wfun 6505   Fn wfn 6506  ⟶wf 6507  –1-1→wf1 6508  –1-1-onto→wf1o 6510

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1ores  6814  f1un  6820  f1cnv  6824  f1cocnv1  6830  f1ocnvfvrneq  7261  fnwelem  8110  oacomf1olem  8528  domss2  9100  ssenen  9115  sucdom2  9167  f1finf1o  9216  f1finf1oOLD  9217  infn0  9251  f1fi  9263  f1dmvrnfibi  9292  marypha1lem  9384  hartogslem1  9495  infdifsn  9610  infxpenlem  9966  infxpenc2lem1  9972  fseqenlem2  9978  ac10ct  9987  acndom  10004  acndom2  10007  dfac12lem2  10098  dfac12lem3  10099  fictb  10197  fin23lem21  10292  axcc2lem  10389  pwfseqlem1  10611  pwfseqlem5  10616  hashf1lem1  14420  hashf1lem2  14421  4sqlem11  16926  xpsff1o2  17532  yoniso  18246  imasmndf1  18703  imasgrpf1  18989  conjsubgen  19183  ghmqusker  19219  cayley  19344  odinf  19493  sylow1lem2  19529  sylow2blem1  19550  gsumval3lem2  19836  gsumval3  19837  dprdf1  19965  imasrngf1  20087  imasringf1  20240  islindf3  21735  uvcf1o  21755  2ndcdisj  23343  dis2ndc  23347  qtopf1  23703  ovolicc2lem4  25421  itg1addlem4  25600  basellem3  26993  fsumvma  27124  dchrisum0fno1  27422  usgrf1o  29098  uspgrf1oedg  29100  usgrf1oedg  29134  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  fnpreimac  32595  fsumiunle  32754  cshf1o  32884  tocycfvres1  33067  tocycfvres2  33068  cycpmfv1  33070  cycpmfv2  33071  cycpmcl  33073  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  tocyccntz  33101  cycpmconjslem1  33111  cycpmconjslem2  33112  idomsubr  33259  dimkerim  33623  esumiun  34084  onvf1od  35094  erdszelem10  35187  mrsubff1o  35502  msubff1o  35544  f1omptsnlem  37324  pibt2  37405  matunitlindflem2  37611  dihcnvcl  41265  dihcnvid1  41266  dihcnvid2  41267  dihlspsnat  41327  dihglblem6  41334  dochocss  41360  dochnoncon  41385  mapdcnvcl  41646  mapdcnvid2  41651  eldioph2lem2  42749  dnwech  43037  cantnfub  43310  disjf1o  45185  f1ocof1ob2  47083  gricushgr  47917  ushggricedg  47927  imaf1homlem  49096  aacllem  49790