Theorem f1f1orn 6791

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 6737	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6503	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6790	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 584	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5630  ran crn 5632  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  –1-1→wf1 6495  –1-1-onto→wf1o 6497

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1ores  6794  f1un  6800  f1cnv  6804  f1cocnv1  6810  f1ocnvfvrneq  7241  fnwelem  8081  oacomf1olem  8499  domss2  9074  ssenen  9089  sucdom2  9137  f1finf1o  9183  infn0  9212  f1fi  9224  f1dmvrnfibi  9251  marypha1lem  9346  hartogslem1  9457  infdifsn  9578  infxpenlem  9935  infxpenc2lem1  9941  fseqenlem2  9947  ac10ct  9956  acndom  9973  acndom2  9976  dfac12lem2  10067  dfac12lem3  10068  fictb  10166  fin23lem21  10261  axcc2lem  10358  pwfseqlem1  10581  pwfseqlem5  10586  hashf1lem1  14417  hashf1lem2  14418  4sqlem11  16926  xpsff1o2  17533  yoniso  18251  imasmndf1  18744  imasgrpf1  19033  conjsubgen  19226  ghmqusker  19262  cayley  19389  odinf  19538  sylow1lem2  19574  sylow2blem1  19595  gsumval3lem2  19881  gsumval3  19882  dprdf1  20010  imasrngf1  20159  imasringf1  20311  islindf3  21806  uvcf1o  21826  2ndcdisj  23421  dis2ndc  23425  qtopf1  23781  ovolicc2lem4  25487  itg1addlem4  25666  basellem3  27046  fsumvma  27176  dchrisum0fno1  27474  usgrf1o  29240  uspgrf1oedg  29242  usgrf1oedg  29276  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  fnpreimac  32743  fsumiunle  32902  cshf1o  33022  tocycfvres1  33171  tocycfvres2  33172  cycpmfv1  33174  cycpmfv2  33175  cycpmcl  33177  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  tocyccntz  33205  cycpmconjslem1  33215  cycpmconjslem2  33216  idomsubr  33370  dimkerim  33771  esumiun  34238  onvf1od  35289  erdszelem10  35382  mrsubff1o  35697  msubff1o  35739  f1omptsnlem  37652  pibt2  37733  matunitlindflem2  37938  dihcnvcl  41717  dihcnvid1  41718  dihcnvid2  41719  dihlspsnat  41779  dihglblem6  41786  dochocss  41812  dochnoncon  41837  mapdcnvcl  42098  mapdcnvid2  42103  eldioph2lem2  43193  dnwech  43476  cantnfub  43749  disjf1o  45621  f1ocof1ob2  47530  gricushgr  48393  ushggricedg  48403  imaf1homlem  49582  aacllem  50276