Theorem f1f1orn 6783

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 6729	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6495	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6782	. 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 5621  ran crn 5623  Fun wfun 6484   Fn wfn 6485  ⟶wf 6486  –1-1→wf1 6487  –1-1-onto→wf1o 6489

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 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2726  df-ss 3916  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1ores  6786  f1un  6792  f1cnv  6796  f1cocnv1  6802  f1ocnvfvrneq  7230  fnwelem  8071  oacomf1olem  8489  domss2  9062  ssenen  9077  sucdom2  9125  f1finf1o  9171  infn0  9200  f1fi  9212  f1dmvrnfibi  9239  marypha1lem  9334  hartogslem1  9445  infdifsn  9564  infxpenlem  9921  infxpenc2lem1  9927  fseqenlem2  9933  ac10ct  9942  acndom  9959  acndom2  9962  dfac12lem2  10053  dfac12lem3  10054  fictb  10152  fin23lem21  10247  axcc2lem  10344  pwfseqlem1  10567  pwfseqlem5  10572  hashf1lem1  14376  hashf1lem2  14377  4sqlem11  16881  xpsff1o2  17488  yoniso  18206  imasmndf1  18699  imasgrpf1  18985  conjsubgen  19178  ghmqusker  19214  cayley  19341  odinf  19490  sylow1lem2  19526  sylow2blem1  19547  gsumval3lem2  19833  gsumval3  19834  dprdf1  19962  imasrngf1  20111  imasringf1  20265  islindf3  21779  uvcf1o  21799  2ndcdisj  23398  dis2ndc  23402  qtopf1  23758  ovolicc2lem4  25475  itg1addlem4  25654  basellem3  27047  fsumvma  27178  dchrisum0fno1  27476  usgrf1o  29193  uspgrf1oedg  29195  usgrf1oedg  29229  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  fnpreimac  32698  fsumiunle  32859  cshf1o  32993  tocycfvres1  33141  tocycfvres2  33142  cycpmfv1  33144  cycpmfv2  33145  cycpmcl  33147  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  tocyccntz  33175  cycpmconjslem1  33185  cycpmconjslem2  33186  idomsubr  33340  dimkerim  33733  esumiun  34200  onvf1od  35250  erdszelem10  35343  mrsubff1o  35658  msubff1o  35700  f1omptsnlem  37480  pibt2  37561  matunitlindflem2  37757  dihcnvcl  41470  dihcnvid1  41471  dihcnvid2  41472  dihlspsnat  41532  dihglblem6  41539  dochocss  41565  dochnoncon  41590  mapdcnvcl  41851  mapdcnvid2  41856  eldioph2lem2  42945  dnwech  43232  cantnfub  43505  disjf1o  45377  f1ocof1ob2  47270  gricushgr  48105  ushggricedg  48115  imaf1homlem  49294  aacllem  49988