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

Definition df-isom 5207
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 5199 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5197 . . 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 3989 . . . . . 6  wff  x R y
139, 5cfv 5198 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5198 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3989 . . . . . 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  5780  isoeq2  5781  isoeq3  5782  isoeq4  5783  isoeq5  5784  nfiso  5785  isof1o  5786  isorel  5787  isoid  5789  isocnv  5790  isocnv2  5791  isores2  5792  isores3  5794  isotr  5795  iso0  5796  isoini2  5798  f1oiso  5805  negiso  8871  frec2uzisod  10363  zfz1isolem1  10775  xrnegiso  11225  reefiso  13492  logltb  13589
  Copyright terms: Public domain W3C validator