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

Theorem isof1o 6802
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 6111 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 492 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wral 3090   class class class wbr 4844  1-1-ontowf1o 6101  cfv 6102   Isom wiso 6103
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 386  df-isom 6111
This theorem is referenced by:  isores1  6813  isomin  6816  isoini  6817  isoini2  6818  isofrlem  6819  isoselem  6820  isofr  6821  isose  6822  isofr2  6823  isopolem  6824  isosolem  6826  weniso  6833  weisoeq  6834  weisoeq2  6835  wemoiso  7387  wemoiso2  7388  smoiso  7699  smoiso2  7706  supisolem  8622  supisoex  8623  supiso  8624  ordiso2  8663  ordtypelem10  8675  oiexg  8683  oien  8686  oismo  8688  cantnfle  8819  cantnflt2  8821  cantnfp1lem3  8828  cantnflem1b  8834  cantnflem1d  8836  cantnflem1  8837  cantnffval2  8843  cantnff1o  8844  wemapwe  8845  cnfcom3lem  8851  infxpenlem  9123  iunfictbso  9224  dfac12lem2  9255  cofsmo  9380  isf34lem3  9486  isf34lem5  9489  hsmexlem1  9537  fpwwe2lem6  9746  fpwwe2lem7  9747  fpwwe2lem9  9749  pwfseqlem5  9774  fz1isolem  13493  seqcoll  13496  seqcoll2  13497  isercolllem2  14736  isercoll  14738  summolem2a  14786  prodmolem2a  15000  gsumval3lem1  18620  gsumval3  18622  ordthmeolem  21932  dvne0f1  24115  dvcvx  24123  isoun  29996  erdsze2lem1  31701  fourierdlem20  41082  fourierdlem50  41111  fourierdlem51  41112  fourierdlem52  41113  fourierdlem63  41124  fourierdlem64  41125  fourierdlem65  41126  fourierdlem76  41137  fourierdlem102  41163  fourierdlem114  41175
  Copyright terms: Public domain W3C validator