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

Definition df-isom 5102
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 5094 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5092 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1315 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1315 . . . . . . 7  class  y
129, 11, 3wbr 3899 . . . . . 6  wff  x R y
139, 5cfv 5093 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5093 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3899 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 104 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2393 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2393 . . 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  5670  isoeq2  5671  isoeq3  5672  isoeq4  5673  isoeq5  5674  nfiso  5675  isof1o  5676  isorel  5677  isoid  5679  isocnv  5680  isocnv2  5681  isores2  5682  isores3  5684  isotr  5685  iso0  5686  isoini2  5688  f1oiso  5695  negiso  8677  frec2uzisod  10135  zfz1isolem1  10538  xrnegiso  10986
  Copyright terms: Public domain W3C validator