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

Theorem f1f1orn 5657
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 5612 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5428 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 464 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5656 . 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 4844   ran crn 4846   Fun wfun 5417    Fn wfn 5418   -->wf 5419   -1-1->wf1 5420   -1-1-onto->wf1o 5422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430
This theorem is referenced by:  f1ores  5660  f1cnv  5669  f1cocnv1  5675  f1ocnvfvrneq  5995  fnwelem  6692  oacomf1olem  7008  domss2  7475  ssenen  7490  sucdom2  7512  f1finf1o  7544  f1fi  7603  marypha1lem  7688  hartogslem1  7761  infdifsn  7867  infxpenlem  8185  infxpenc2lem1  8190  fseqenlem2  8200  ac10ct  8209  acndom  8226  acndom2  8229  dfac12lem2  8318  dfac12lem3  8319  fictb  8419  fin23lem21  8513  axcc2lem  8610  pwfseqlem1  8830  pwfseqlem5  8835  hashf1lem1  12213  hashf1lem2  12214  4sqlem11  14021  xpsff1o2  14514  yoniso  15100  imasmndf1  15465  imasgrpf1  15677  conjsubgen  15784  cayley  15924  odinf  16069  sylow1lem2  16103  sylow2blem1  16124  gsumval3OLD  16387  gsumval3lem1  16388  gsumval3lem2  16389  gsumval3  16390  dprdf1  16535  islindf3  18260  uvcf1o  18280  2ndcdisj  19065  dis2ndc  19069  qtopf1  19394  ovolicc2lem4  21008  itg1addlem4  21182  basellem3  22425  fsumvma  22557  dchrisum0fno1  22765  usgraf1o  23286  constr3trllem1  23541  constr3trllem5  23545  erdszelem10  27093  eldioph2lem2  29104  dnwech  29406  dihcnvcl  34921  dihcnvid1  34922  dihcnvid2  34923  dihlspsnat  34983  dihglblem6  34990  dochocss  35016  dochnoncon  35041  mapdcnvcl  35302  mapdcnvid2  35307
  Copyright terms: Public domain W3C validator