ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-isom Unicode version

Definition df-isom 5011
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 5003 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5001 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1288 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1288 . . . . . . 7  class  y
129, 11, 3wbr 3837 . . . . . 6  wff  x R y
139, 5cfv 5002 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5002 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3837 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 103 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2359 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2359 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 102 . 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 103 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  5562  isoeq2  5563  isoeq3  5564  isoeq4  5565  isoeq5  5566  nfiso  5567  isof1o  5568  isorel  5569  isoid  5571  isocnv  5572  isocnv2  5573  isores2  5574  isores3  5576  isotr  5577  iso0  5578  isoini2  5580  f1oiso  5587  negiso  8388  frec2uzisod  9779  zfz1isolem1  10210
  Copyright terms: Public domain W3C validator