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

Theorem f1f1orn 5677
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 5632 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5451 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 451 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5676 . 2  |-  ( F : A -1-1-onto-> ran  F  <->  ( F  Fn  A  /\  Fun  `' F ) )
51, 3, 4sylanbrc 646 1  |-  ( F : A -1-1-> B  ->  F : A -1-1-onto-> ran  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4869   ran crn 4871   Fun wfun 5440    Fn wfn 5441   -->wf 5442   -1-1->wf1 5443   -1-1-onto->wf1o 5445
This theorem is referenced by:  f1ores  5681  f1cnv  5691  f1cocnv1  5697  f1ocnvfvrneq  6011  fnwelem  6453  oacomf1olem  6799  domss2  7258  ssenen  7273  sucdom2  7295  f1finf1o  7327  f1fi  7385  marypha1lem  7430  hartogslem1  7501  infdifsn  7601  infxpenlem  7885  infxpenc2lem1  7890  fseqenlem2  7896  ac10ct  7905  acndom  7922  acndom2  7925  dfac12lem2  8014  dfac12lem3  8015  fictb  8115  fin23lem21  8209  axcc2lem  8306  pwfseqlem1  8523  pwfseqlem5  8528  hashf1lem1  11694  hashf1lem2  11695  4sqlem11  13313  xpsff1o2  13786  yoniso  14372  imasmndf1  14724  imasgrpf1  14925  conjsubgen  15028  cayley  15102  odinf  15189  sylow1lem2  15223  sylow2blem1  15244  gsumval3  15504  dprdf1  15581  2ndcdisj  17509  dis2ndc  17513  qtopf1  17838  ovolicc2lem4  19406  itg1addlem4  19581  basellem3  20855  fsumvma  20987  dchrisum0fno1  21195  usgraf1o  21372  constr3trllem1  21627  constr3trllem5  21631  erdszelem10  24876  eldioph2lem2  26773  dnwech  27077  islindf3  27228  dihcnvcl  31970  dihcnvid1  31971  dihcnvid2  31972  dihlspsnat  32032  dihglblem6  32039  dochocss  32065  dochnoncon  32090  mapdcnvcl  32351  mapdcnvid2  32356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453
  Copyright terms: Public domain W3C validator