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

Theorem f1f1orn 5626
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 5581 . 2  |-  ( F : A -1-1-> B  ->  F  Fn  A )
2 df-f1 5400 . . 3  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 451 . 2  |-  ( F : A -1-1-> B  ->  Fun  `' F )
4 f1orn 5625 . 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 4818   ran crn 4820   Fun wfun 5389    Fn wfn 5390   -->wf 5391   -1-1->wf1 5392   -1-1-onto->wf1o 5394
This theorem is referenced by:  f1ores  5630  f1cnv  5640  f1cocnv1  5646  f1ocnvfvrneq  5959  fnwelem  6398  oacomf1olem  6744  domss2  7203  ssenen  7218  sucdom2  7240  f1finf1o  7272  f1fi  7330  marypha1lem  7374  hartogslem1  7445  infdifsn  7545  infxpenlem  7829  infxpenc2lem1  7834  fseqenlem2  7840  ac10ct  7849  acndom  7866  acndom2  7869  dfac12lem2  7958  dfac12lem3  7959  fictb  8059  fin23lem21  8153  axcc2lem  8250  pwfseqlem1  8467  pwfseqlem5  8472  hashf1rn  11564  hashf1lem1  11632  hashf1lem2  11633  4sqlem11  13251  xpsff1o2  13724  yoniso  14310  imasmndf1  14662  imasgrpf1  14863  conjsubgen  14966  cayley  15040  odinf  15127  sylow1lem2  15161  sylow2blem1  15182  gsumval3  15442  dprdf1  15519  2ndcdisj  17441  dis2ndc  17445  qtopf1  17770  ovolicc2lem4  19284  itg1addlem4  19459  basellem3  20733  fsumvma  20865  dchrisum0fno1  21073  usgraf1o  21250  constr3trllem1  21486  constr3trllem5  21490  erdszelem10  24666  eldioph2lem2  26511  dnwech  26815  islindf3  26966  dihcnvcl  31387  dihcnvid1  31388  dihcnvid2  31389  dihlspsnat  31449  dihglblem6  31456  dochocss  31482  dochnoncon  31507  mapdcnvcl  31768  mapdcnvid2  31773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-in 3271  df-ss 3278  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402
  Copyright terms: Public domain W3C validator