Theorem f1f1orn 6855

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-1ontoran 𝐹)

Proof of Theorem f1f1orn

Step	Hyp	Ref	Expression
1		f1fn 6798	. 2 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6560	. . 3 ⊢ (𝐹:𝐴⟶1-1𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 503	. 2 ⊢ (𝐹:𝐴⟶1-1𝐵 → Fun ◡𝐹)
4		f1orn 6854	. 2 ⊢ (𝐹:𝐴⟶1-1ontoran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 595	1 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹:𝐴⟶1-1ontoran 𝐹)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5654  ran crn 5656  Fun wfun 6549   Fn wfn 6550  ⟶wf 6551  ⟶1-1wf1 6552  ⟶1-1ontowf1o 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562

This theorem is used by:  f1ores  6858  f1un  6864  f1cnv  6868  f1cocnv1  6875  f1ocnvfvrneq  7314  f1we  7383  fnwelem  8167  oacomf1olem  8597  domss2  9180  ssenen  9195  sucdom2  9243  f1finf1o  9289  infn0  9319  f1fi  9331  f1dmvrnfibi  9355  marypha1lem  9449  hartogslem1  9560  infdifsn  9682  infxpenlem  10116  infxpenc2lem1  10122  fseqenlem2  10128  acndom  10154  acndom2  10157  dfac12lem2  10247  dfac12lem3  10248  fictb  10346  fin23lem21  10441  axcc2lem  10538  pwfseqlem1  10767  pwfseqlem5  10772  hashf1lem1  14624  hashf1lem2  14625  4sqlem11  17159  xpsff1o2  17767  yoniso  18485  imasmndf1  18996  imasgrpf1  19293  conjsubgen  19491  ghmqusker  19528  cayley  19655  odinf  19804  sylow1lem2  19840  sylow2blem1  19861  gsumval3lem2  20147  gsumval3  20148  dprdf1  20276  imasrngf1  20427  imasringf1  20588  islindf3  22159  uvcf1o  22179  matunitlindflem2  23022  2ndcdisj  23802  dis2ndc  23806  qtopf1  24162  ovolicc2lem4  25868  itg1addlem4  26047  basellem3  27437  fsumvma  27567  dchrisum0fno1  27865  usgrf1o  29779  uspgrf1oedg  29781  usgrf1oedg  29815  clwlkclwwlklem2a4  30615  clwlkclwwlklem2a  30616  fnpreimac  33333  fsumiunle  33487  cshf1o  33590  tocycfvres1  33738  tocycfvres2  33739  cycpmfv1  33741  cycpmfv2  33742  cycpmcl  33744  cycpmco2lem4  33757  cycpmco2lem5  33758  cycpmco2lem6  33759  cycpmco2lem7  33760  cycpmco2  33761  tocyccntz  33772  cycpmconjslem1  33782  cycpmconjslem2  33783  idomsubr  33938  dimkerim  34326  esumiun  34793  onf1we  35800  onvf1od  36034  onprcf1acwevd  36046  prconf1acwevd  36047  erdszelem10  36131  mrsubff1o  36446  msubff1o  36488  f1omptsnlem  38450  pibt2  38531  dihcnvcl  42519  dihcnvid1  42520  dihcnvid2  42521  dihlspsnat  42581  dihglblem6  42588  dochocss  42614  dochnoncon  42639  mapdcnvcl  42900  mapdcnvid2  42905  eldioph2lem2  43963  cantnfub  44513  disjf1o  46409  f1ocof1ob2  48355  gricushgr  49218  ushggricedg  49228  imaf1homlem  50426  aacllem  51217