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

Theorem f1f1orn 5817
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 5772 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5583 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 464 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5816 . 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 4988   ran crn 4990   Fun wfun 5572    Fn wfn 5573   -->wf 5574   -1-1->wf1 5575   -1-1-onto->wf1o 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585
This theorem is referenced by:  f1ores  5820  f1cnv  5829  f1cocnv1  5835  f1ocnvfvrneq  6174  fnwelem  6900  oacomf1olem  7215  domss2  7678  ssenen  7693  sucdom2  7716  f1finf1o  7748  f1fi  7809  marypha1lem  7895  hartogslem1  7970  infdifsn  8076  infxpenlem  8394  infxpenc2lem1  8399  fseqenlem2  8409  ac10ct  8418  acndom  8435  acndom2  8438  dfac12lem2  8527  dfac12lem3  8528  fictb  8628  fin23lem21  8722  axcc2lem  8819  pwfseqlem1  9039  pwfseqlem5  9044  hashf1lem1  12486  hashf1lem2  12487  4sqlem11  14455  xpsff1o2  14950  yoniso  15533  imasmndf1  15938  imasgrpf1  16166  conjsubgen  16278  cayley  16418  odinf  16564  sylow1lem2  16598  sylow2blem1  16619  gsumval3OLD  16887  gsumval3lem1  16888  gsumval3lem2  16889  gsumval3  16890  dprdf1  17059  islindf3  18839  uvcf1o  18859  2ndcdisj  19935  dis2ndc  19939  qtopf1  20295  ovolicc2lem4  21909  itg1addlem4  22084  basellem3  23334  fsumvma  23466  dchrisum0fno1  23674  usgraf1o  24336  uslgraf1oedg  24337  constr3trllem1  24628  constr3trllem5  24632  erdszelem10  28622  mrsubff1o  28853  msubff1o  28895  eldioph2lem2  30670  dnwech  30970  f1dmvrnfibi  32266  dihcnvcl  36873  dihcnvid1  36874  dihcnvid2  36875  dihlspsnat  36935  dihglblem6  36942  dochocss  36968  dochnoncon  36993  mapdcnvcl  37254  mapdcnvid2  37259
  Copyright terms: Public domain W3C validator