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

Theorem f1f1orn 6046
Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
Assertion
Ref Expression
f1f1orn (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)

Proof of Theorem f1f1orn
StepHypRef Expression
1 f1fn 6000 . 2 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
2 df-f1 5795 . . 3 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
32simprbi 478 . 2 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
4 f1orn 6045 . 2 (𝐹:𝐴1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹))
51, 3, 4sylanbrc 694 1 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5027  ran crn 5029  Fun wfun 5784   Fn wfn 5785  wf 5786  1-1wf1 5787  1-1-ontowf1o 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797
This theorem is referenced by:  f1ores  6049  f1cnv  6058  f1cocnv1  6064  f1ocnvfvrneq  6419  fnwelem  7156  oacomf1olem  7508  domss2  7981  ssenen  7996  sucdom2  8018  f1finf1o  8049  f1dmvrnfibi  8110  f1fi  8113  marypha1lem  8199  hartogslem1  8307  infdifsn  8414  infxpenlem  8696  infxpenc2lem1  8702  fseqenlem2  8708  ac10ct  8717  acndom  8734  acndom2  8737  dfac12lem2  8826  dfac12lem3  8827  fictb  8927  fin23lem21  9021  axcc2lem  9118  pwfseqlem1  9336  pwfseqlem5  9341  hashf1lem1  13048  hashf1lem2  13049  4sqlem11  15443  xpsff1o2  16000  yoniso  16694  imasmndf1  17098  imasgrpf1  17301  conjsubgen  17462  cayley  17603  odinf  17749  sylow1lem2  17783  sylow2blem1  17804  gsumval3lem1  18075  gsumval3lem2  18076  gsumval3  18077  dprdf1  18201  islindf3  19926  uvcf1o  19946  2ndcdisj  21011  dis2ndc  21015  qtopf1  21371  ovolicc2lem4  23012  itg1addlem4  23189  basellem3  24526  fsumvma  24655  dchrisum0fno1  24917  usgraf1o  25653  uslgraf1oedg  25654  constr3trllem1  25944  constr3trllem5  25948  esumiun  29289  erdszelem10  30242  mrsubff1o  30472  msubff1o  30514  f1omptsnlem  32162  matunitlindflem2  32379  dihcnvcl  35381  dihcnvid1  35382  dihcnvid2  35383  dihlspsnat  35443  dihglblem6  35450  dochocss  35476  dochnoncon  35501  mapdcnvcl  35762  mapdcnvid2  35767  eldioph2lem2  36145  dnwech  36439  disjf1o  38176  usgrf1o  40403  uspgrf1oedg  40405  usgrf1oedg  40436  clwlkclwwlklem2a4  41208  clwlkclwwlklem2a  41209  aacllem  42319
  Copyright terms: Public domain W3C validator