Theorem f1f1orn 6628

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 6578	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6362	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 499	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6627	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 585	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5556  ran crn 5558  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353  –1-1→wf1 6354  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  f1ores  6631  f1cnv  6640  f1cocnv1  6646  f1ocnvfvrneq  7044  fnwelem  7827  oacomf1olem  8192  domss2  8678  ssenen  8693  sucdom2  8716  f1finf1o  8747  f1dmvrnfibi  8810  f1fi  8813  marypha1lem  8899  hartogslem1  9008  infdifsn  9122  infxpenlem  9441  infxpenc2lem1  9447  fseqenlem2  9453  ac10ct  9462  acndom  9479  acndom2  9482  dfac12lem2  9572  dfac12lem3  9573  fictb  9669  fin23lem21  9763  axcc2lem  9860  pwfseqlem1  10082  pwfseqlem5  10087  hashf1lem1  13816  hashf1lem2  13817  4sqlem11  16293  xpsff1o2  16844  yoniso  17537  imasmndf1  17952  imasgrpf1  18218  conjsubgen  18393  cayley  18544  odinf  18692  sylow1lem2  18726  sylow2blem1  18747  gsumval3lem2  19028  gsumval3  19029  dprdf1  19157  islindf3  20972  uvcf1o  20992  2ndcdisj  22066  dis2ndc  22070  qtopf1  22426  ovolicc2lem4  24123  itg1addlem4  24302  basellem3  25662  fsumvma  25791  dchrisum0fno1  26089  usgrf1o  26958  uspgrf1oedg  26960  usgrf1oedg  26991  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  fnpreimac  30418  fsumiunle  30547  cshf1o  30638  tocycfvres1  30754  tocycfvres2  30755  cycpmfv1  30757  cycpmfv2  30758  cycpmcl  30760  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  tocyccntz  30788  cycpmconjslem1  30798  cycpmconjslem2  30799  dimkerim  31025  esumiun  31355  erdszelem10  32449  mrsubff1o  32764  msubff1o  32806  f1omptsnlem  34619  pibt2  34700  matunitlindflem2  34891  dihcnvcl  38409  dihcnvid1  38410  dihcnvid2  38411  dihlspsnat  38471  dihglblem6  38478  dochocss  38504  dochnoncon  38529  mapdcnvcl  38790  mapdcnvid2  38795  eldioph2lem2  39365  dnwech  39655  disjf1o  41459  isomushgr  43998  ushrisomgr  44013  aacllem  44909