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

Theorem isof1o 6074
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 5492 . 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 448 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wral 2711   class class class wbr 4237   -1-1-onto->wf1o 5482   ` cfv 5483    Isom wiso 5484
This theorem is referenced by:  isores1  6083  isomin  6086  isoini  6087  isoini2  6088  isofrlem  6089  isoselem  6090  isofr  6091  isose  6092  isofr2  6093  isopolem  6094  isosolem  6096  weniso  6104  weisoeq  6105  weisoeq2  6106  wemoiso  6107  wemoiso2  6108  smoiso  6653  smoiso2  6660  supisolem  7504  supisoex  7505  supiso  7506  ordiso2  7513  ordtypelem10  7525  oiexg  7533  oien  7536  oismo  7538  cantnfle  7655  cantnflt2  7657  cantnfp1lem3  7665  cantnflem1b  7671  cantnflem1d  7673  cantnflem1  7674  cantnffval2  7680  cantnff1o  7681  wemapwe  7683  cnfcom3lem  7689  infxpenlem  7926  iunfictbso  8026  dfac12lem2  8055  cofsmo  8180  isf34lem3  8286  isf34lem5  8289  hsmexlem1  8337  fpwwe2lem6  8541  fpwwe2lem7  8542  fpwwe2lem9  8544  pwfseqlem5  8569  fz1isolem  11741  seqcoll  11743  seqcoll2  11744  isercolllem2  12490  isercoll  12492  summolem2a  12540  gsumval3  15545  ordthmeolem  17864  dvne0f1  19927  dvcvx  19935  isoun  24120  erdsze2lem1  24920  prodmolem2a  25291
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 179  df-an 362  df-isom 5492
  Copyright terms: Public domain W3C validator