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

Definition df-isom 5466
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 5458 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5456 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1652 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1652 . . . . . . 7  class  y
129, 11, 3wbr 4215 . . . . . 6  wff  x R y
139, 5cfv 5457 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5457 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4215 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 178 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2707 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2707 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 360 . 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 178 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  6042  isoeq2  6043  isoeq3  6044  isoeq4  6045  isoeq5  6046  nfiso  6047  isof1o  6048  isorel  6049  soisores  6050  soisoi  6051  isoid  6052  isocnv  6053  isocnv2  6054  isocnv3  6055  isores2  6056  isores3  6058  isotr  6059  isoini2  6062  f1oiso  6074  f1owe  6076  smoiso2  6634  alephiso  7984  compssiso  8259  negiso  9989  om2uzisoi  11299  icopnfhmeo  18973  reefiso  20369  logltb  20499  isoun  24094  xrmulc1cn  24321  wepwsolem  27130  iso0  27527
  Copyright terms: Public domain W3C validator