Theorem f1f1orn 6494

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 6444	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6230	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6493	. 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 5442  ran crn 5444  Fun wfun 6219   Fn wfn 6220  ⟶wf 6221  –1-1→wf1 6222  –1-1-onto→wf1o 6224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232

This theorem is referenced by:  f1ores  6497  f1cnv  6506  f1cocnv1  6512  f1ocnvfvrneq  6907  fnwelem  7678  oacomf1olem  8040  domss2  8523  ssenen  8538  sucdom2  8560  f1finf1o  8591  f1dmvrnfibi  8654  f1fi  8657  marypha1lem  8743  hartogslem1  8852  infdifsn  8966  infxpenlem  9285  infxpenc2lem1  9291  fseqenlem2  9297  ac10ct  9306  acndom  9323  acndom2  9326  dfac12lem2  9416  dfac12lem3  9417  fictb  9513  fin23lem21  9607  axcc2lem  9704  pwfseqlem1  9926  pwfseqlem5  9931  hashf1lem1  13661  hashf1lem2  13662  4sqlem11  16120  xpsff1o2  16671  yoniso  17364  imasmndf1  17768  imasgrpf1  17973  conjsubgen  18132  cayley  18273  odinf  18420  sylow1lem2  18454  sylow2blem1  18475  gsumval3lem2  18747  gsumval3  18748  dprdf1  18872  islindf3  20652  uvcf1o  20672  2ndcdisj  21748  dis2ndc  21752  qtopf1  22108  ovolicc2lem4  23804  itg1addlem4  23983  basellem3  25342  fsumvma  25471  dchrisum0fno1  25769  usgrf1o  26639  uspgrf1oedg  26641  usgrf1oedg  26672  clwlkclwwlklem2a4  27462  clwlkclwwlklem2a  27463  fnpreimac  30106  fsumiunle  30229  cshf1o  30310  tocycfvres1  30399  tocycfvres2  30400  cycpmfv1  30402  cycpmfv2  30403  cycpmcl  30405  tocyccntz  30423  cycpmconjslem1  30434  cycpmconjslem2  30435  dimkerim  30627  esumiun  30970  erdszelem10  32055  mrsubff1o  32370  msubff1o  32412  f1omptsnlem  34148  pibt2  34229  matunitlindflem2  34420  dihcnvcl  37938  dihcnvid1  37939  dihcnvid2  37940  dihlspsnat  38000  dihglblem6  38007  dochocss  38033  dochnoncon  38058  mapdcnvcl  38319  mapdcnvid2  38324  eldioph2lem2  38843  dnwech  39133  disjf1o  40992  isomushgr  43473  ushrisomgr  43488  aacllem  44382