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

Definition df-isom 5455
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 5447 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5445 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1651 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1651 . . . . . . 7  class  y
129, 11, 3wbr 4204 . . . . . 6  wff  x R y
139, 5cfv 5446 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5446 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4204 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 177 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2697 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2697 . . 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  6031  isoeq2  6032  isoeq3  6033  isoeq4  6034  isoeq5  6035  nfiso  6036  isof1o  6037  isorel  6038  soisores  6039  soisoi  6040  isoid  6041  isocnv  6042  isocnv2  6043  isocnv3  6044  isores2  6045  isores3  6047  isotr  6048  isoini2  6051  f1oiso  6063  f1owe  6065  smoiso2  6623  alephiso  7971  compssiso  8246  negiso  9976  om2uzisoi  11286  icopnfhmeo  18960  reefiso  20356  logltb  20486  isoun  24081  xrmulc1cn  24308  wepwsolem  27107  iso0  27504
  Copyright terms: Public domain W3C validator