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

Definition df-isom 5404
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 5396 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5394 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1648 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1648 . . . . . . 7  class  y
129, 11, 3wbr 4154 . . . . . 6  wff  x R y
139, 5cfv 5395 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5395 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4154 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 177 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2650 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2650 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 359 . 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 177 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 set class
This definition is referenced by:  isoeq1  5979  isoeq2  5980  isoeq3  5981  isoeq4  5982  isoeq5  5983  nfiso  5984  isof1o  5985  isorel  5986  soisores  5987  soisoi  5988  isoid  5989  isocnv  5990  isocnv2  5991  isocnv3  5992  isores2  5993  isores3  5995  isotr  5996  isoini2  5999  f1oiso  6011  f1owe  6013  smoiso2  6568  alephiso  7913  compssiso  8188  negiso  9917  om2uzisoi  11222  icopnfhmeo  18840  reefiso  20232  logltb  20362  isoun  23931  xrmulc1cn  24121  wepwsolem  26808  iso0  27206
  Copyright terms: Public domain W3C validator