Theorem f1f1orn 6820

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 6763	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6528	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 501	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6819	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 592	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5648  ran crn 5650  Fun wfun 6517   Fn wfn 6518  ⟶wf 6519  –1-1→wf1 6520  –1-1-onto→wf1o 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-ex 1802  df-cleq 2756  df-ss 3923  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530

This theorem is referenced by:  f1ores  6823  f1un  6829  f1cnv  6833  f1cocnv1  6839  f1ocnvfvrneq  7272  fnwelem  8113  oacomf1olem  8535  domss2  9110  ssenen  9125  sucdom2  9173  f1finf1o  9219  infn0  9248  f1fi  9260  f1dmvrnfibi  9286  marypha1lem  9381  hartogslem1  9492  infdifsn  9614  infxpenlem  9971  infxpenc2lem1  9977  fseqenlem2  9983  ac10ct  9992  acndom  10009  acndom2  10012  dfac12lem2  10103  dfac12lem3  10104  fictb  10202  fin23lem21  10298  axcc2lem  10395  pwfseqlem1  10618  pwfseqlem5  10623  hashf1lem1  14470  hashf1lem2  14471  4sqlem11  16993  xpsff1o2  17601  yoniso  18319  imasmndf1  18812  imasgrpf1  19101  conjsubgen  19293  ghmqusker  19329  cayley  19456  odinf  19605  sylow1lem2  19641  sylow2blem1  19662  gsumval3lem2  19948  gsumval3  19949  dprdf1  20077  imasrngf1  20226  imasringf1  20382  islindf3  21880  uvcf1o  21900  2ndcdisj  23518  dis2ndc  23522  qtopf1  23878  ovolicc2lem4  25584  itg1addlem4  25763  basellem3  27149  fsumvma  27279  dchrisum0fno1  27577  usgrf1o  29374  uspgrf1oedg  29376  usgrf1oedg  29410  clwlkclwwlklem2a4  30201  clwlkclwwlklem2a  30202  fnpreimac  32874  fsumiunle  33033  cshf1o  33142  tocycfvres1  33292  tocycfvres2  33293  cycpmfv1  33295  cycpmfv2  33296  cycpmcl  33298  cycpmco2lem4  33311  cycpmco2lem5  33312  cycpmco2lem6  33313  cycpmco2lem7  33314  cycpmco2  33315  tocyccntz  33326  cycpmconjslem1  33336  cycpmconjslem2  33337  idomsubr  33498  dimkerim  33926  esumiun  34393  onvf1od  35454  erdszelem10  35555  mrsubff1o  35870  msubff1o  35912  f1omptsnlem  37835  pibt2  37916  matunitlindflem2  38121  dihcnvcl  41900  dihcnvid1  41901  dihcnvid2  41902  dihlspsnat  41962  dihglblem6  41969  dochocss  41995  dochnoncon  42020  mapdcnvcl  42281  mapdcnvid2  42286  eldioph2lem2  43347  dnwech  43630  cantnfub  43903  disjf1o  45774  f1ocof1ob2  47681  gricushgr  48544  ushggricedg  48554  imaf1homlem  49733  aacllem  50427