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

Theorem f1f1orn 6186
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 6140 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 df-f1 5931 . . 3 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
32simprbi 479 . 2 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
4 f1orn 6185 . 2 (𝐹:𝐴1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹))
51, 3, 4sylanbrc 699 1 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5142  ran crn 5144  Fun wfun 5920   Fn wfn 5921  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1ores  6189  f1cnv  6198  f1cocnv1  6204  f1ocnvfvrneq  6581  fnwelem  7337  oacomf1olem  7689  domss2  8160  ssenen  8175  sucdom2  8197  f1finf1o  8228  f1dmvrnfibi  8291  f1fi  8294  marypha1lem  8380  hartogslem1  8488  infdifsn  8592  infxpenlem  8874  infxpenc2lem1  8880  fseqenlem2  8886  ac10ct  8895  acndom  8912  acndom2  8915  dfac12lem2  9004  dfac12lem3  9005  fictb  9105  fin23lem21  9199  axcc2lem  9296  pwfseqlem1  9518  pwfseqlem5  9523  hashf1lem1  13277  hashf1lem2  13278  4sqlem11  15706  xpsff1o2  16278  yoniso  16972  imasmndf1  17376  imasgrpf1  17579  conjsubgen  17740  cayley  17880  odinf  18026  sylow1lem2  18060  sylow2blem1  18081  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  dprdf1  18478  islindf3  20213  uvcf1o  20233  2ndcdisj  21307  dis2ndc  21311  qtopf1  21667  ovolicc2lem4  23334  itg1addlem4  23511  basellem3  24854  fsumvma  24983  dchrisum0fno1  25245  usgrf1o  26111  uspgrf1oedg  26113  usgrf1oedg  26144  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  fsumiunle  29703  esumiun  30284  erdszelem10  31308  mrsubff1o  31538  msubff1o  31580  f1omptsnlem  33313  matunitlindflem2  33536  dihcnvcl  36877  dihcnvid1  36878  dihcnvid2  36879  dihlspsnat  36939  dihglblem6  36946  dochocss  36972  dochnoncon  36997  mapdcnvcl  37258  mapdcnvid2  37263  eldioph2lem2  37641  dnwech  37935  disjf1o  39692  aacllem  42875
  Copyright terms: Public domain W3C validator