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

Definition df-isom 5205
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 5197 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5195 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1347 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1347 . . . . . . 7  class  y
129, 11, 3wbr 3987 . . . . . 6  wff  x R y
139, 5cfv 5196 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5196 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3987 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 104 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2448 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2448 . . 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  5778  isoeq2  5779  isoeq3  5780  isoeq4  5781  isoeq5  5782  nfiso  5783  isof1o  5784  isorel  5785  isoid  5787  isocnv  5788  isocnv2  5789  isores2  5790  isores3  5792  isotr  5793  iso0  5794  isoini2  5796  f1oiso  5803  negiso  8864  frec2uzisod  10356  zfz1isolem1  10768  xrnegiso  11218  reefiso  13457  logltb  13554
  Copyright terms: Public domain W3C validator