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

Theorem isof1o 6036
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 5454 . 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 447 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2697   class class class wbr 4204   -1-1-onto->wf1o 5444   ` cfv 5445    Isom wiso 5446
This theorem is referenced by:  isores1  6045  isomin  6048  isoini  6049  isoini2  6050  isofrlem  6051  isoselem  6052  isofr  6053  isose  6054  isofr2  6055  isopolem  6056  isosolem  6058  weniso  6066  weisoeq  6067  weisoeq2  6068  wemoiso  6069  wemoiso2  6070  smoiso  6615  smoiso2  6622  supisolem  7464  supisoex  7465  supiso  7466  ordiso2  7473  ordtypelem10  7485  oiexg  7493  oien  7496  oismo  7498  cantnfle  7615  cantnflt2  7617  cantnfp1lem3  7625  cantnflem1b  7631  cantnflem1d  7633  cantnflem1  7634  cantnffval2  7640  cantnff1o  7641  wemapwe  7643  cnfcom3lem  7649  infxpenlem  7884  iunfictbso  7984  dfac12lem2  8013  cofsmo  8138  isf34lem3  8244  isf34lem5  8247  hsmexlem1  8295  fpwwe2lem6  8499  fpwwe2lem7  8500  fpwwe2lem9  8502  pwfseqlem5  8527  fz1isolem  11698  seqcoll  11700  seqcoll2  11701  isercolllem2  12447  isercoll  12449  summolem2a  12497  gsumval3  15502  ordthmeolem  17821  dvne0f1  19884  dvcvx  19892  isoun  24077  erdsze2lem1  24877  prodmolem2a  25249
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 178  df-an 361  df-isom 5454
  Copyright terms: Public domain W3C validator