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

Definition df-isom 5505
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 5497 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5495 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1398 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1398 . . . . . . 7  class  y
129, 11, 3wbr 4367 . . . . . 6  wff  x R y
139, 5cfv 5496 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5496 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4367 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 184 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2732 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2732 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 367 . 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  6116  isoeq2  6117  isoeq3  6118  isoeq4  6119  isoeq5  6120  nfiso  6121  isof1o  6122  isorel  6123  soisores  6124  soisoi  6125  isoid  6126  isocnv  6127  isocnv2  6128  isocnv3  6129  isores2  6130  isores3  6132  isotr  6133  isoini2  6136  f1oiso  6148  f1owe  6150  smoiso2  6958  alephiso  8392  compssiso  8667  negiso  10435  om2uzisoi  11968  icopnfhmeo  21528  reefiso  22928  logltb  23072  isoun  27667  xrmulc1cn  28066  wepwsolem  31153  iso0  31355  fourierdlem54  32109
  Copyright terms: Public domain W3C validator