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

Theorem f1f1orn 5499
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 5454 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5276 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 450 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5498 . 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 4704   ran crn 4706   Fun wfun 5265    Fn wfn 5266   -->wf 5267   -1-1->wf1 5268   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1ores  5503  f1cnv  5513  f1cocnv1  5519  fnwelem  6246  oacomf1olem  6578  domss2  7036  ssenen  7051  sucdom2  7073  f1finf1o  7102  f1fi  7159  marypha1lem  7202  hartogslem1  7273  infdifsn  7373  infxpenlem  7657  infxpenc2lem1  7662  fseqenlem2  7668  ac10ct  7677  acndom  7694  acndom2  7697  dfac12lem2  7786  dfac12lem3  7787  fictb  7887  fin23lem21  7981  axcc2lem  8078  pwfseqlem1  8296  pwfseqlem5  8301  hashf1lem1  11409  hashf1lem2  11410  4sqlem11  13018  xpsff1o2  13489  yoniso  14075  imasmndf1  14427  imasgrpf1  14628  conjsubgen  14731  cayley  14805  odinf  14892  sylow1lem2  14926  sylow2blem1  14947  gsumval3  15207  dprdf1  15284  2ndcdisj  17198  dis2ndc  17202  qtopf1  17523  ovolicc2lem4  18895  itg1addlem4  19070  basellem3  20336  fsumvma  20468  dchrisum0fno1  20676  erdszelem10  23746  eldioph2lem2  26943  dnwech  27248  islindf3  27399  f1ocnvfvrneq  28189  usgraf1o  28242  constr3trllem1  28396  constr3trllem2  28397  constr3trllem5  28400  dihcnvcl  32083  dihcnvid1  32084  dihcnvid2  32085  dihlspsnat  32145  dihglblem6  32152  dochocss  32178  dochnoncon  32203  mapdcnvcl  32464  mapdcnvid2  32469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278
  Copyright terms: Public domain W3C validator