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

Definition df-isom 4941
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 4933 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 4931 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1284 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1284 . . . . . . 7  class  y
129, 11, 3wbr 3793 . . . . . 6  wff  x R y
139, 5cfv 4932 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 4932 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3793 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 103 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2349 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2349 . . 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  5472  isoeq2  5473  isoeq3  5474  isoeq4  5475  isoeq5  5476  nfiso  5477  isof1o  5478  isorel  5479  isoid  5481  isocnv  5482  isocnv2  5483  isores2  5484  isores3  5486  isotr  5487  isoini2  5489  f1oiso  5496  negiso  8100  frec2uzisod  9489
  Copyright terms: Public domain W3C validator