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

Definition df-isom 5610
Description: Define the isomorphism predicate. We read this as "
H is an  R,  S isomorphism of  A onto  B." Normally,  R and  S are ordering relations on  A and  B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that  R and  S are subscripts. (Contributed by NM, 4-Mar-1997.)
Assertion
Ref Expression
df-isom  |-  ( 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 ) ) ) )
Distinct variable groups:    x, y, A    x, B, y    x, R, y    x, S, y   
x, H, y

Detailed syntax breakdown of Definition df-isom
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
4 cS . . 3  class  S
5 cH . . 3  class  H
61, 2, 3, 4, 5wiso 5602 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5600 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1436 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1436 . . . . . . 7  class  y
129, 11, 3wbr 4426 . . . . . 6  wff  x R y
139, 5cfv 5601 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5601 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4426 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 187 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2782 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2782 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 370 . 2  wff  ( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) ) )
206, 19wb 187 1  wff  ( 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 ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  6225  isoeq2  6226  isoeq3  6227  isoeq4  6228  isoeq5  6229  nfiso  6230  isof1o  6231  isorel  6232  soisores  6233  soisoi  6234  isoid  6235  isocnv  6236  isocnv2  6237  isocnv3  6238  isores2  6239  isores3  6241  isotr  6242  isoini2  6245  f1oiso  6257  f1owe  6259  smoiso2  7096  alephiso  8527  compssiso  8802  negiso  10587  om2uzisoi  12165  icopnfhmeo  21867  reefiso  23268  logltb  23414  isoun  28122  xrmulc1cn  28575  wepwsolem  35605  iso0  36291  fourierdlem54  37591
  Copyright terms: Public domain W3C validator