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

Definition df-isom 5587
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 5579 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5577 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1382 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1382 . . . . . . 7  class  y
129, 11, 3wbr 4437 . . . . . 6  wff  x R y
139, 5cfv 5578 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5578 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4437 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 184 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2793 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2793 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 369 . 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 184 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  6200  isoeq2  6201  isoeq3  6202  isoeq4  6203  isoeq5  6204  nfiso  6205  isof1o  6206  isorel  6207  soisores  6208  soisoi  6209  isoid  6210  isocnv  6211  isocnv2  6212  isocnv3  6213  isores2  6214  isores3  6216  isotr  6217  isoini2  6220  f1oiso  6232  f1owe  6234  smoiso2  7042  alephiso  8482  compssiso  8757  negiso  10526  om2uzisoi  12047  icopnfhmeo  21421  reefiso  22821  logltb  22962  isoun  27498  xrmulc1cn  27890  wepwsolem  30963  iso0  31163  fourierdlem54  31897
  Copyright terms: Public domain W3C validator