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

Theorem isof1o 5838
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 5280 . 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 2556   class class class wbr 4039   -1-1-onto->wf1o 5270   ` cfv 5271    Isom wiso 5272
This theorem is referenced by:  isores1  5847  isomin  5850  isoini  5851  isoini2  5852  isofrlem  5853  isoselem  5854  isofr  5855  isose  5856  isofr2  5857  isopolem  5858  isosolem  5860  weniso  5868  weisoeq  5869  weisoeq2  5870  wemoiso  5871  wemoiso2  5872  smoiso  6395  smoiso2  6402  supisolem  7237  supisoex  7238  supiso  7239  ordiso2  7246  ordtypelem10  7258  oiexg  7266  oien  7269  oismo  7271  cantnfle  7388  cantnflt2  7390  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cantnffval2  7413  cantnff1o  7414  wemapwe  7416  cnfcom3lem  7422  infxpenlem  7657  iunfictbso  7757  dfac12lem2  7786  cofsmo  7911  isf34lem3  8017  isf34lem5  8020  hsmexlem1  8068  fpwwe2lem6  8273  fpwwe2lem7  8274  fpwwe2lem9  8276  pwfseqlem5  8301  fz1isolem  11415  seqcoll  11417  seqcoll2  11418  isercolllem2  12155  isercoll  12157  summolem2a  12204  gsumval3  15207  ordthmeolem  17508  dvne0f1  19375  dvcvx  19383  isoun  23257  erdsze2lem1  23749  prodmolem2a  24157
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 5280
  Copyright terms: Public domain W3C validator