Theorem f1f1orn 6842

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 6786	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 6546	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 498	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6841	. 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 5675  ran crn 5677  Fun wfun 6535   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538  –1-1-onto→wf1o 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is referenced by:  f1ores  6845  f1un  6851  f1cnv  6855  f1cocnv1  6861  f1ocnvfvrneq  7281  fnwelem  8114  oacomf1olem  8561  sucdom2OLD  9079  domss2  9133  ssenen  9148  sucdom2  9203  f1finf1o  9268  f1finf1oOLD  9269  infn0  9304  f1dmvrnfibi  9333  f1fi  9336  marypha1lem  9425  hartogslem1  9534  infdifsn  9649  infxpenlem  10005  infxpenc2lem1  10011  fseqenlem2  10017  ac10ct  10026  acndom  10043  acndom2  10046  dfac12lem2  10136  dfac12lem3  10137  fictb  10237  fin23lem21  10331  axcc2lem  10428  pwfseqlem1  10650  pwfseqlem5  10655  hashf1lem1  14412  hashf1lem1OLD  14413  hashf1lem2  14414  4sqlem11  16885  xpsff1o2  17512  yoniso  18235  imasmndf1  18661  imasgrpf1  18937  conjsubgen  19120  cayley  19277  odinf  19426  sylow1lem2  19462  sylow2blem1  19483  gsumval3lem2  19769  gsumval3  19770  dprdf1  19898  imasringf1  20138  islindf3  21373  uvcf1o  21393  2ndcdisj  22952  dis2ndc  22956  qtopf1  23312  ovolicc2lem4  25029  itg1addlem4  25208  itg1addlem4OLD  25209  basellem3  26577  fsumvma  26706  dchrisum0fno1  27004  usgrf1o  28421  uspgrf1oedg  28423  usgrf1oedg  28454  clwlkclwwlklem2a4  29240  clwlkclwwlklem2a  29241  fnpreimac  31884  fsumiunle  32023  cshf1o  32114  tocycfvres1  32257  tocycfvres2  32258  cycpmfv1  32260  cycpmfv2  32261  cycpmcl  32263  cycpmco2lem4  32276  cycpmco2lem5  32277  cycpmco2lem6  32278  cycpmco2lem7  32279  cycpmco2  32280  tocyccntz  32291  cycpmconjslem1  32301  cycpmconjslem2  32302  ghmqusker  32521  dimkerim  32701  esumiun  33081  erdszelem10  34180  mrsubff1o  34495  msubff1o  34537  f1omptsnlem  36206  pibt2  36287  matunitlindflem2  36474  dihcnvcl  40131  dihcnvid1  40132  dihcnvid2  40133  dihlspsnat  40193  dihglblem6  40200  dochocss  40226  dochnoncon  40251  mapdcnvcl  40512  mapdcnvid2  40517  eldioph2lem2  41485  dnwech  41776  cantnfub  42057  disjf1o  43875  f1ocof1ob2  45777  isomushgr  46481  ushrisomgr  46496  imasrngf1  46666  aacllem  47802