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

Theorem f1f1orn 6796
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 6740 . 2 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹 Fn 𝐴)
2 df-f1 6502 . . 3 (𝐹:𝐴–1-1→𝐡 ↔ (𝐹:𝐴⟢𝐡 ∧ Fun ◑𝐹))
32simprbi 498 . 2 (𝐹:𝐴–1-1→𝐡 β†’ Fun ◑𝐹)
4 f1orn 6795 . 2 (𝐹:𝐴–1-1-ontoβ†’ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◑𝐹))
51, 3, 4sylanbrc 584 1 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4  β—‘ccnv 5633  ran crn 5635  Fun wfun 6491   Fn wfn 6492  βŸΆwf 6493  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1ores  6799  f1un  6805  f1cnv  6809  f1cocnv1  6815  f1ocnvfvrneq  7233  fnwelem  8064  oacomf1olem  8512  sucdom2OLD  9027  domss2  9081  ssenen  9096  sucdom2  9151  f1finf1o  9216  f1finf1oOLD  9217  infn0  9252  f1dmvrnfibi  9281  f1fi  9284  marypha1lem  9370  hartogslem1  9479  infdifsn  9594  infxpenlem  9950  infxpenc2lem1  9956  fseqenlem2  9962  ac10ct  9971  acndom  9988  acndom2  9991  dfac12lem2  10081  dfac12lem3  10082  fictb  10182  fin23lem21  10276  axcc2lem  10373  pwfseqlem1  10595  pwfseqlem5  10600  hashf1lem1  14354  hashf1lem1OLD  14355  hashf1lem2  14356  4sqlem11  16828  xpsff1o2  17452  yoniso  18175  imasmndf1  18596  imasgrpf1  18865  conjsubgen  19042  cayley  19197  odinf  19346  sylow1lem2  19382  sylow2blem1  19403  gsumval3lem2  19684  gsumval3  19685  dprdf1  19813  islindf3  21235  uvcf1o  21255  2ndcdisj  22810  dis2ndc  22814  qtopf1  23170  ovolicc2lem4  24887  itg1addlem4  25066  itg1addlem4OLD  25067  basellem3  26435  fsumvma  26564  dchrisum0fno1  26862  usgrf1o  28125  uspgrf1oedg  28127  usgrf1oedg  28158  clwlkclwwlklem2a4  28944  clwlkclwwlklem2a  28945  fnpreimac  31590  fsumiunle  31728  cshf1o  31819  tocycfvres1  31962  tocycfvres2  31963  cycpmfv1  31965  cycpmfv2  31966  cycpmcl  31968  cycpmco2lem4  31981  cycpmco2lem5  31982  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmco2  31985  tocyccntz  31996  cycpmconjslem1  32006  cycpmconjslem2  32007  ghmqusker  32201  dimkerim  32325  esumiun  32696  erdszelem10  33797  mrsubff1o  34112  msubff1o  34154  f1omptsnlem  35810  pibt2  35891  matunitlindflem2  36078  dihcnvcl  39737  dihcnvid1  39738  dihcnvid2  39739  dihlspsnat  39799  dihglblem6  39806  dochocss  39832  dochnoncon  39857  mapdcnvcl  40118  mapdcnvid2  40123  eldioph2lem2  41087  dnwech  41378  cantnfub  41658  disjf1o  43417  f1ocof1ob2  45321  isomushgr  46025  ushrisomgr  46040  aacllem  47255
  Copyright terms: Public domain W3C validator