Theorem f1f1orn 6829

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 6775	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6536	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6828	. 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 5653  ran crn 5655  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  –1-1→wf1 6528  –1-1-onto→wf1o 6530

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is referenced by:  f1ores  6832  f1un  6838  f1cnv  6842  f1cocnv1  6848  f1ocnvfvrneq  7279  fnwelem  8130  oacomf1olem  8576  sucdom2OLD  9096  domss2  9150  ssenen  9165  sucdom2  9217  f1finf1o  9277  f1finf1oOLD  9278  infn0  9312  f1fi  9324  f1dmvrnfibi  9353  marypha1lem  9445  hartogslem1  9556  infdifsn  9671  infxpenlem  10027  infxpenc2lem1  10033  fseqenlem2  10039  ac10ct  10048  acndom  10065  acndom2  10068  dfac12lem2  10159  dfac12lem3  10160  fictb  10258  fin23lem21  10353  axcc2lem  10450  pwfseqlem1  10672  pwfseqlem5  10677  hashf1lem1  14473  hashf1lem2  14474  4sqlem11  16975  xpsff1o2  17583  yoniso  18297  imasmndf1  18754  imasgrpf1  19040  conjsubgen  19234  ghmqusker  19270  cayley  19395  odinf  19544  sylow1lem2  19580  sylow2blem1  19601  gsumval3lem2  19887  gsumval3  19888  dprdf1  20016  imasrngf1  20138  imasringf1  20291  islindf3  21786  uvcf1o  21806  2ndcdisj  23394  dis2ndc  23398  qtopf1  23754  ovolicc2lem4  25473  itg1addlem4  25652  basellem3  27045  fsumvma  27176  dchrisum0fno1  27474  usgrf1o  29150  uspgrf1oedg  29152  usgrf1oedg  29186  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  fnpreimac  32649  fsumiunle  32808  cshf1o  32938  tocycfvres1  33121  tocycfvres2  33122  cycpmfv1  33124  cycpmfv2  33125  cycpmcl  33127  cycpmco2lem4  33140  cycpmco2lem5  33141  cycpmco2lem6  33142  cycpmco2lem7  33143  cycpmco2  33144  tocyccntz  33155  cycpmconjslem1  33165  cycpmconjslem2  33166  idomsubr  33303  dimkerim  33667  esumiun  34125  erdszelem10  35222  mrsubff1o  35537  msubff1o  35579  f1omptsnlem  37354  pibt2  37435  matunitlindflem2  37641  dihcnvcl  41290  dihcnvid1  41291  dihcnvid2  41292  dihlspsnat  41352  dihglblem6  41359  dochocss  41385  dochnoncon  41410  mapdcnvcl  41671  mapdcnvid2  41676  eldioph2lem2  42784  dnwech  43072  cantnfub  43345  disjf1o  45215  f1ocof1ob2  47111  gricushgr  47930  ushggricedg  47940  imaf1homlem  49066  aacllem  49665