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

Definition df-isom 5264
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 5256 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5254 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1622 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1622 . . . . . . 7  class  y
129, 11, 3wbr 4023 . . . . . 6  wff  x R y
139, 5cfv 5255 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5255 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4023 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 176 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2543 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2543 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 358 . 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 176 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  5816  isoeq2  5817  isoeq3  5818  isoeq4  5819  isoeq5  5820  nfiso  5821  isof1o  5822  isorel  5823  soisores  5824  soisoi  5825  isoid  5826  isocnv  5827  isocnv2  5828  isocnv3  5829  isores2  5830  isores3  5832  isotr  5833  isoini2  5836  f1oiso  5848  f1owe  5850  smoiso2  6386  alephiso  7725  compssiso  8000  negiso  9730  om2uzisoi  11017  icopnfhmeo  18441  reefiso  19824  logltb  19953  wepwsolem  26550  iso0  26948
  Copyright terms: Public domain W3C validator