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

Definition df-isom 5068
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 5060 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5058 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1298 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1298 . . . . . . 7  class  y
129, 11, 3wbr 3875 . . . . . 6  wff  x R y
139, 5cfv 5059 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5059 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3875 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 104 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2375 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2375 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 103 . 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 104 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  5634  isoeq2  5635  isoeq3  5636  isoeq4  5637  isoeq5  5638  nfiso  5639  isof1o  5640  isorel  5641  isoid  5643  isocnv  5644  isocnv2  5645  isores2  5646  isores3  5648  isotr  5649  iso0  5650  isoini2  5652  f1oiso  5659  negiso  8571  frec2uzisod  10021  zfz1isolem1  10424  xrnegiso  10870
  Copyright terms: Public domain W3C validator