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

Theorem f1f1orn 5483
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 5438 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5260 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 450 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5482 . 2  |-  ( F : A -1-1-onto-> ran  F  <->  ( F  Fn  A  /\  Fun  `' F ) )
51, 3, 4sylanbrc 645 1  |-  ( F : A -1-1-> B  ->  F : A -1-1-onto-> ran  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4688   ran crn 4690   Fun wfun 5249    Fn wfn 5250   -->wf 5251   -1-1->wf1 5252   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1ores  5487  f1cnv  5497  f1cocnv1  5503  fnwelem  6230  oacomf1olem  6562  domss2  7020  ssenen  7035  sucdom2  7057  f1finf1o  7086  f1fi  7143  marypha1lem  7186  hartogslem1  7257  infdifsn  7357  infxpenlem  7641  infxpenc2lem1  7646  fseqenlem2  7652  ac10ct  7661  acndom  7678  acndom2  7681  dfac12lem2  7770  dfac12lem3  7771  fictb  7871  fin23lem21  7965  axcc2lem  8062  pwfseqlem1  8280  pwfseqlem5  8285  hashf1lem1  11393  hashf1lem2  11394  4sqlem11  13002  xpsff1o2  13473  yoniso  14059  imasmndf1  14411  imasgrpf1  14612  conjsubgen  14715  cayley  14789  odinf  14876  sylow1lem2  14910  sylow2blem1  14931  gsumval3  15191  dprdf1  15268  2ndcdisj  17182  dis2ndc  17186  qtopf1  17507  ovolicc2lem4  18879  itg1addlem4  19054  basellem3  20320  fsumvma  20452  dchrisum0fno1  20660  erdszelem10  23731  eldioph2lem2  26840  dnwech  27145  islindf3  27296  dihcnvcl  31461  dihcnvid1  31462  dihcnvid2  31463  dihlspsnat  31523  dihglblem6  31530  dochocss  31556  dochnoncon  31581  mapdcnvcl  31842  mapdcnvid2  31847
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator