Theorem f1f1orn 6148

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 6102	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 5893	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 480	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6147	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 698	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5113  ran crn 5115  Fun wfun 5882   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1ores  6151  f1cnv  6160  f1cocnv1  6166  f1ocnvfvrneq  6541  fnwelem  7292  oacomf1olem  7644  domss2  8119  ssenen  8134  sucdom2  8156  f1finf1o  8187  f1dmvrnfibi  8250  f1fi  8253  marypha1lem  8339  hartogslem1  8447  infdifsn  8554  infxpenlem  8836  infxpenc2lem1  8842  fseqenlem2  8848  ac10ct  8857  acndom  8874  acndom2  8877  dfac12lem2  8966  dfac12lem3  8967  fictb  9067  fin23lem21  9161  axcc2lem  9258  pwfseqlem1  9480  pwfseqlem5  9485  hashf1lem1  13239  hashf1lem2  13240  4sqlem11  15659  xpsff1o2  16231  yoniso  16925  imasmndf1  17329  imasgrpf1  17532  conjsubgen  17693  cayley  17834  odinf  17980  sylow1lem2  18014  sylow2blem1  18035  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  dprdf1  18432  islindf3  20165  uvcf1o  20185  2ndcdisj  21259  dis2ndc  21263  qtopf1  21619  ovolicc2lem4  23288  itg1addlem4  23466  basellem3  24809  fsumvma  24938  dchrisum0fno1  25200  usgrf1o  26066  uspgrf1oedg  26068  usgrf1oedg  26099  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  fsumiunle  29575  esumiun  30156  erdszelem10  31182  mrsubff1o  31412  msubff1o  31454  f1omptsnlem  33183  matunitlindflem2  33406  dihcnvcl  36560  dihcnvid1  36561  dihcnvid2  36562  dihlspsnat  36622  dihglblem6  36629  dochocss  36655  dochnoncon  36680  mapdcnvcl  36941  mapdcnvid2  36946  eldioph2lem2  37324  dnwech  37618  disjf1o  39378  aacllem  42547