Theorem f1f1orn 6873

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 6818	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6578	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 496	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6872	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 582	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5699  ran crn 5701  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  –1-1→wf1 6570  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  f1ores  6876  f1un  6882  f1cnv  6886  f1cocnv1  6892  f1ocnvfvrneq  7322  fnwelem  8172  oacomf1olem  8620  sucdom2OLD  9148  domss2  9202  ssenen  9217  sucdom2  9269  f1finf1o  9333  f1finf1oOLD  9334  infn0  9368  f1fi  9380  f1dmvrnfibi  9409  marypha1lem  9502  hartogslem1  9611  infdifsn  9726  infxpenlem  10082  infxpenc2lem1  10088  fseqenlem2  10094  ac10ct  10103  acndom  10120  acndom2  10123  dfac12lem2  10214  dfac12lem3  10215  fictb  10313  fin23lem21  10408  axcc2lem  10505  pwfseqlem1  10727  pwfseqlem5  10732  hashf1lem1  14504  hashf1lem2  14505  4sqlem11  17002  xpsff1o2  17629  yoniso  18355  imasmndf1  18811  imasgrpf1  19097  conjsubgen  19291  ghmqusker  19327  cayley  19456  odinf  19605  sylow1lem2  19641  sylow2blem1  19662  gsumval3lem2  19948  gsumval3  19949  dprdf1  20077  imasrngf1  20205  imasringf1  20354  islindf3  21869  uvcf1o  21889  2ndcdisj  23485  dis2ndc  23489  qtopf1  23845  ovolicc2lem4  25574  itg1addlem4  25753  itg1addlem4OLD  25754  basellem3  27144  fsumvma  27275  dchrisum0fno1  27573  usgrf1o  29206  uspgrf1oedg  29208  usgrf1oedg  29242  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  fnpreimac  32689  fsumiunle  32833  cshf1o  32929  tocycfvres1  33103  tocycfvres2  33104  cycpmfv1  33106  cycpmfv2  33107  cycpmcl  33109  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  tocyccntz  33137  cycpmconjslem1  33147  cycpmconjslem2  33148  idomsubr  33276  dimkerim  33640  esumiun  34058  erdszelem10  35168  mrsubff1o  35483  msubff1o  35525  f1omptsnlem  37302  pibt2  37383  matunitlindflem2  37577  dihcnvcl  41228  dihcnvid1  41229  dihcnvid2  41230  dihlspsnat  41290  dihglblem6  41297  dochocss  41323  dochnoncon  41348  mapdcnvcl  41609  mapdcnvid2  41614  eldioph2lem2  42717  dnwech  43005  cantnfub  43283  disjf1o  45098  f1ocof1ob2  46997  gricushgr  47770  ushggricedg  47780  aacllem  48895