Theorem f1f1orn 6061

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 6015	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 5809	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 479	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 6060	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 695	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Syntax hints:   → wi 4  ^◡ccnv 5037  ran crn 5039  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –1-1-onto→wf1o 5803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811

This theorem is referenced by:  f1ores  6064  f1cnv  6073  f1cocnv1  6079  f1ocnvfvrneq  6441  fnwelem  7179  oacomf1olem  7531  domss2  8004  ssenen  8019  sucdom2  8041  f1finf1o  8072  f1dmvrnfibi  8133  f1fi  8136  marypha1lem  8222  hartogslem1  8330  infdifsn  8437  infxpenlem  8719  infxpenc2lem1  8725  fseqenlem2  8731  ac10ct  8740  acndom  8757  acndom2  8760  dfac12lem2  8849  dfac12lem3  8850  fictb  8950  fin23lem21  9044  axcc2lem  9141  pwfseqlem1  9359  pwfseqlem5  9364  hashf1lem1  13096  hashf1lem2  13097  4sqlem11  15497  xpsff1o2  16054  yoniso  16748  imasmndf1  17152  imasgrpf1  17355  conjsubgen  17516  cayley  17657  odinf  17803  sylow1lem2  17837  sylow2blem1  17858  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  dprdf1  18255  islindf3  19984  uvcf1o  20004  2ndcdisj  21069  dis2ndc  21073  qtopf1  21429  ovolicc2lem4  23095  itg1addlem4  23272  basellem3  24609  fsumvma  24738  dchrisum0fno1  25000  usgraf1o  25887  uslgraf1oedg  25888  constr3trllem1  26178  constr3trllem5  26182  esumiun  29483  erdszelem10  30436  mrsubff1o  30666  msubff1o  30708  f1omptsnlem  32359  matunitlindflem2  32576  dihcnvcl  35578  dihcnvid1  35579  dihcnvid2  35580  dihlspsnat  35640  dihglblem6  35647  dochocss  35673  dochnoncon  35698  mapdcnvcl  35959  mapdcnvid2  35964  eldioph2lem2  36342  dnwech  36636  disjf1o  38373  usgrf1o  40401  uspgrf1oedg  40403  usgrf1oedg  40434  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  aacllem  42356