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

Theorem f1f1orn 5827
Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
Assertion
Ref Expression
f1f1orn  |-  ( F : A -1-1-> B  ->  F : A -1-1-onto-> ran  F )

Proof of Theorem f1f1orn
StepHypRef Expression
1 f1fn 5782 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5593 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 464 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5826 . 2  |-  ( F : A -1-1-onto-> ran  F  <->  ( F  Fn  A  /\  Fun  `' F ) )
51, 3, 4sylanbrc 664 1  |-  ( F : A -1-1-> B  ->  F : A -1-1-onto-> ran  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   `'ccnv 4998   ran crn 5000   Fun wfun 5582    Fn wfn 5583   -->wf 5584   -1-1->wf1 5585   -1-1-onto->wf1o 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595
This theorem is referenced by:  f1ores  5830  f1cnv  5839  f1cocnv1  5845  f1ocnvfvrneq  6177  fnwelem  6898  oacomf1olem  7213  domss2  7676  ssenen  7691  sucdom2  7714  f1finf1o  7746  f1fi  7807  marypha1lem  7893  hartogslem1  7967  infdifsn  8073  infxpenlem  8391  infxpenc2lem1  8396  fseqenlem2  8406  ac10ct  8415  acndom  8432  acndom2  8435  dfac12lem2  8524  dfac12lem3  8525  fictb  8625  fin23lem21  8719  axcc2lem  8816  pwfseqlem1  9036  pwfseqlem5  9041  hashf1lem1  12470  hashf1lem2  12471  4sqlem11  14332  xpsff1o2  14826  yoniso  15412  imasmndf1  15778  imasgrpf1  15997  conjsubgen  16104  cayley  16244  odinf  16391  sylow1lem2  16425  sylow2blem1  16446  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  gsumval3  16714  dprdf1  16882  islindf3  18656  uvcf1o  18676  2ndcdisj  19751  dis2ndc  19755  qtopf1  20080  ovolicc2lem4  21694  itg1addlem4  21869  basellem3  23112  fsumvma  23244  dchrisum0fno1  23452  usgraf1o  24062  uslgraf1oedg  24063  constr3trllem1  24354  constr3trllem5  24358  erdszelem10  28312  eldioph2lem2  30326  dnwech  30626  f1dmvrnfibi  31807  dihcnvcl  36086  dihcnvid1  36087  dihcnvid2  36088  dihlspsnat  36148  dihglblem6  36155  dochocss  36181  dochnoncon  36206  mapdcnvcl  36467  mapdcnvid2  36472
  Copyright terms: Public domain W3C validator