MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1f1orn Structured version   Visualization version   GIF version

Theorem f1f1orn 6115
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
StepHypRef Expression
1 f1fn 6069 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 df-f1 5862 . . 3 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
32simprbi 480 . 2 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
4 f1orn 6114 . 2 (𝐹:𝐴1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹))
51, 3, 4sylanbrc 697 1 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5083  ran crn 5085  Fun wfun 5851   Fn wfn 5852  wf 5853  1-1wf1 5854  1-1-ontowf1o 5856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864
This theorem is referenced by:  f1ores  6118  f1cnv  6127  f1cocnv1  6133  f1ocnvfvrneq  6506  fnwelem  7252  oacomf1olem  7604  domss2  8079  ssenen  8094  sucdom2  8116  f1finf1o  8147  f1dmvrnfibi  8210  f1fi  8213  marypha1lem  8299  hartogslem1  8407  infdifsn  8514  infxpenlem  8796  infxpenc2lem1  8802  fseqenlem2  8808  ac10ct  8817  acndom  8834  acndom2  8837  dfac12lem2  8926  dfac12lem3  8927  fictb  9027  fin23lem21  9121  axcc2lem  9218  pwfseqlem1  9440  pwfseqlem5  9445  hashf1lem1  13193  hashf1lem2  13194  4sqlem11  15602  xpsff1o2  16171  yoniso  16865  imasmndf1  17269  imasgrpf1  17472  conjsubgen  17633  cayley  17774  odinf  17920  sylow1lem2  17954  sylow2blem1  17975  gsumval3lem1  18246  gsumval3lem2  18247  gsumval3  18248  dprdf1  18372  islindf3  20105  uvcf1o  20125  2ndcdisj  21199  dis2ndc  21203  qtopf1  21559  ovolicc2lem4  23228  itg1addlem4  23406  basellem3  24743  fsumvma  24872  dchrisum0fno1  25134  usgrf1o  25993  uspgrf1oedg  25995  usgrf1oedg  26026  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  esumiun  29979  erdszelem10  30943  mrsubff1o  31173  msubff1o  31215  f1omptsnlem  32854  matunitlindflem2  33077  dihcnvcl  36079  dihcnvid1  36080  dihcnvid2  36081  dihlspsnat  36141  dihglblem6  36148  dochocss  36174  dochnoncon  36199  mapdcnvcl  36460  mapdcnvid2  36465  eldioph2lem2  36843  dnwech  37137  disjf1o  38887  aacllem  41880
  Copyright terms: Public domain W3C validator