Theorem f1f1orn 6859

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 6805	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6567	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6858	. 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 5687  ran crn 5689  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  –1-1→wf1 6559  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1ores  6862  f1un  6868  f1cnv  6872  f1cocnv1  6878  f1ocnvfvrneq  7305  fnwelem  8154  oacomf1olem  8600  sucdom2OLD  9120  domss2  9174  ssenen  9189  sucdom2  9240  f1finf1o  9302  f1finf1oOLD  9303  infn0  9337  f1fi  9349  f1dmvrnfibi  9378  marypha1lem  9470  hartogslem1  9579  infdifsn  9694  infxpenlem  10050  infxpenc2lem1  10056  fseqenlem2  10062  ac10ct  10071  acndom  10088  acndom2  10091  dfac12lem2  10182  dfac12lem3  10183  fictb  10281  fin23lem21  10376  axcc2lem  10473  pwfseqlem1  10695  pwfseqlem5  10700  hashf1lem1  14490  hashf1lem2  14491  4sqlem11  16988  xpsff1o2  17615  yoniso  18341  imasmndf1  18801  imasgrpf1  19087  conjsubgen  19281  ghmqusker  19317  cayley  19446  odinf  19595  sylow1lem2  19631  sylow2blem1  19652  gsumval3lem2  19938  gsumval3  19939  dprdf1  20067  imasrngf1  20195  imasringf1  20344  islindf3  21863  uvcf1o  21883  2ndcdisj  23479  dis2ndc  23483  qtopf1  23839  ovolicc2lem4  25568  itg1addlem4  25747  itg1addlem4OLD  25748  basellem3  27140  fsumvma  27271  dchrisum0fno1  27569  usgrf1o  29202  uspgrf1oedg  29204  usgrf1oedg  29238  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  fnpreimac  32687  fsumiunle  32835  cshf1o  32931  tocycfvres1  33112  tocycfvres2  33113  cycpmfv1  33115  cycpmfv2  33116  cycpmcl  33118  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmco2  33135  tocyccntz  33146  cycpmconjslem1  33156  cycpmconjslem2  33157  idomsubr  33290  dimkerim  33654  esumiun  34074  erdszelem10  35184  mrsubff1o  35499  msubff1o  35541  f1omptsnlem  37318  pibt2  37399  matunitlindflem2  37603  dihcnvcl  41253  dihcnvid1  41254  dihcnvid2  41255  dihlspsnat  41315  dihglblem6  41322  dochocss  41348  dochnoncon  41373  mapdcnvcl  41634  mapdcnvid2  41639  eldioph2lem2  42748  dnwech  43036  cantnfub  43310  disjf1o  45133  f1ocof1ob2  47031  gricushgr  47823  ushggricedg  47833  aacllem  49031