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

Theorem isof1o 6828
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isof1o (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)

Proof of Theorem isof1o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 6132 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 493 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wral 3117   class class class wbr 4873  1-1-ontowf1o 6122  cfv 6123   Isom wiso 6124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 199  df-an 387  df-isom 6132
This theorem is referenced by:  isores1  6839  isomin  6842  isoini  6843  isoini2  6844  isofrlem  6845  isoselem  6846  isofr  6847  isose  6848  isofr2  6849  isopolem  6850  isosolem  6852  weniso  6859  weisoeq  6860  weisoeq2  6861  wemoiso  7413  wemoiso2  7414  smoiso  7725  smoiso2  7732  supisolem  8648  supisoex  8649  supiso  8650  ordiso2  8689  ordtypelem10  8701  oiexg  8709  oien  8712  oismo  8714  cantnfle  8845  cantnflt2  8847  cantnfp1lem3  8854  cantnflem1b  8860  cantnflem1d  8862  cantnflem1  8863  cantnffval2  8869  cantnff1o  8870  wemapwe  8871  cnfcom3lem  8877  infxpenlem  9149  iunfictbso  9250  dfac12lem2  9281  cofsmo  9406  isf34lem3  9512  isf34lem5  9515  hsmexlem1  9563  fpwwe2lem6  9772  fpwwe2lem7  9773  fpwwe2lem9  9775  pwfseqlem5  9800  fz1isolem  13534  seqcoll  13537  seqcoll2  13538  isercolllem2  14773  isercoll  14775  summolem2a  14823  prodmolem2a  15037  gsumval3lem1  18659  gsumval3  18661  ordthmeolem  21975  dvne0f1  24174  dvcvx  24182  isoun  30027  erdsze2lem1  31731  fourierdlem20  41138  fourierdlem50  41167  fourierdlem51  41168  fourierdlem52  41169  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem76  41193  fourierdlem102  41219  fourierdlem114  41231
  Copyright terms: Public domain W3C validator