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

Theorem isof1o 6570
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 5895 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 476 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2911   class class class wbr 4651  1-1-ontowf1o 5885  cfv 5886   Isom wiso 5887
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 197  df-an 386  df-isom 5895
This theorem is referenced by:  isores1  6581  isomin  6584  isoini  6585  isoini2  6586  isofrlem  6587  isoselem  6588  isofr  6589  isose  6590  isofr2  6591  isopolem  6592  isosolem  6594  weniso  6601  weisoeq  6602  weisoeq2  6603  wemoiso  7150  wemoiso2  7151  smoiso  7456  smoiso2  7463  supisolem  8376  supisoex  8377  supiso  8378  ordiso2  8417  ordtypelem10  8429  oiexg  8437  oien  8440  oismo  8442  cantnfle  8565  cantnflt2  8567  cantnfp1lem3  8574  cantnflem1b  8580  cantnflem1d  8582  cantnflem1  8583  cantnffval2  8589  cantnff1o  8590  wemapwe  8591  cnfcom3lem  8597  infxpenlem  8833  iunfictbso  8934  dfac12lem2  8963  cofsmo  9088  isf34lem3  9194  isf34lem5  9197  hsmexlem1  9245  fpwwe2lem6  9454  fpwwe2lem7  9455  fpwwe2lem9  9457  pwfseqlem5  9482  fz1isolem  13240  seqcoll  13243  seqcoll2  13244  isercolllem2  14390  isercoll  14392  summolem2a  14440  prodmolem2a  14658  gsumval3lem1  18300  gsumval3  18302  ordthmeolem  21598  dvne0f1  23769  dvcvx  23777  isoun  29464  erdsze2lem1  31170  fourierdlem20  40113  fourierdlem50  40142  fourierdlem51  40143  fourierdlem52  40144  fourierdlem63  40155  fourierdlem64  40156  fourierdlem65  40157  fourierdlem76  40168  fourierdlem102  40194  fourierdlem114  40206
  Copyright terms: Public domain W3C validator