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

Theorem isof1o 5822
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isof1o  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)

Proof of Theorem isof1o
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 5264 . 2  |-  ( H 
Isom  R ,  S  ( A ,  B )  <-> 
( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
21simplbi 446 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543   class class class wbr 4023   -1-1-onto->wf1o 5254   ` cfv 5255    Isom wiso 5256
This theorem is referenced by:  isores1  5831  isomin  5834  isoini  5835  isoini2  5836  isofrlem  5837  isoselem  5838  isofr  5839  isose  5840  isofr2  5841  isopolem  5842  isosolem  5844  weniso  5852  weisoeq  5853  weisoeq2  5854  wemoiso  5855  wemoiso2  5856  smoiso  6379  smoiso2  6386  supisolem  7221  supisoex  7222  supiso  7223  ordiso2  7230  ordtypelem10  7242  oiexg  7250  oien  7253  oismo  7255  cantnfle  7372  cantnflt2  7374  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cantnffval2  7397  cantnff1o  7398  wemapwe  7400  cnfcom3lem  7406  infxpenlem  7641  iunfictbso  7741  dfac12lem2  7770  cofsmo  7895  isf34lem3  8001  isf34lem5  8004  hsmexlem1  8052  fpwwe2lem6  8257  fpwwe2lem7  8258  fpwwe2lem9  8260  pwfseqlem5  8285  fz1isolem  11399  seqcoll  11401  seqcoll2  11402  isercolllem2  12139  isercoll  12141  summolem2a  12188  gsumval3  15191  ordthmeolem  17492  dvne0f1  19359  dvcvx  19367  isoun  23242  erdsze2lem1  23734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-isom 5264
  Copyright terms: Public domain W3C validator