Theorem f1f1orn 6787

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 6733	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6499	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6786	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 584	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5625  ran crn 5627  Fun wfun 6488   Fn wfn 6489  ⟶wf 6490  –1-1→wf1 6491  –1-1-onto→wf1o 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501

This theorem is referenced by:  f1ores  6790  f1un  6796  f1cnv  6800  f1cocnv1  6806  f1ocnvfvrneq  7236  fnwelem  8076  oacomf1olem  8494  domss2  9069  ssenen  9084  sucdom2  9132  f1finf1o  9178  infn0  9207  f1fi  9219  f1dmvrnfibi  9246  marypha1lem  9341  hartogslem1  9452  infdifsn  9573  infxpenlem  9930  infxpenc2lem1  9936  fseqenlem2  9942  ac10ct  9951  acndom  9968  acndom2  9971  dfac12lem2  10062  dfac12lem3  10063  fictb  10161  fin23lem21  10256  axcc2lem  10353  pwfseqlem1  10576  pwfseqlem5  10581  hashf1lem1  14412  hashf1lem2  14413  4sqlem11  16921  xpsff1o2  17528  yoniso  18246  imasmndf1  18739  imasgrpf1  19028  conjsubgen  19221  ghmqusker  19257  cayley  19384  odinf  19533  sylow1lem2  19569  sylow2blem1  19590  gsumval3lem2  19876  gsumval3  19877  dprdf1  20005  imasrngf1  20154  imasringf1  20306  islindf3  21820  uvcf1o  21840  2ndcdisj  23435  dis2ndc  23439  qtopf1  23795  ovolicc2lem4  25501  itg1addlem4  25680  basellem3  27064  fsumvma  27194  dchrisum0fno1  27492  usgrf1o  29258  uspgrf1oedg  29260  usgrf1oedg  29294  clwlkclwwlklem2a4  30086  clwlkclwwlklem2a  30087  fnpreimac  32762  fsumiunle  32921  cshf1o  33041  tocycfvres1  33190  tocycfvres2  33191  cycpmfv1  33193  cycpmfv2  33194  cycpmcl  33196  cycpmco2lem4  33209  cycpmco2lem5  33210  cycpmco2lem6  33211  cycpmco2lem7  33212  cycpmco2  33213  tocyccntz  33224  cycpmconjslem1  33234  cycpmconjslem2  33235  idomsubr  33389  dimkerim  33791  esumiun  34258  onvf1od  35309  erdszelem10  35402  mrsubff1o  35717  msubff1o  35759  f1omptsnlem  37670  pibt2  37751  matunitlindflem2  37956  dihcnvcl  41735  dihcnvid1  41736  dihcnvid2  41737  dihlspsnat  41797  dihglblem6  41804  dochocss  41830  dochnoncon  41855  mapdcnvcl  42116  mapdcnvid2  42121  eldioph2lem2  43211  dnwech  43498  cantnfub  43771  disjf1o  45643  f1ocof1ob2  47546  gricushgr  48409  ushggricedg  48419  imaf1homlem  49598  aacllem  50292