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

Definition df-isom 5237
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 5229 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5227 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1362 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1362 . . . . . . 7  class  y
129, 11, 3wbr 4015 . . . . . 6  wff  x R y
139, 5cfv 5228 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5228 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4015 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 105 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2465 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2465 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 104 . 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 105 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  5815  isoeq2  5816  isoeq3  5817  isoeq4  5818  isoeq5  5819  nfiso  5820  isof1o  5821  isorel  5822  isoid  5824  isocnv  5825  isocnv2  5826  isores2  5827  isores3  5829  isotr  5830  iso0  5831  isoini2  5833  f1oiso  5840  negiso  8926  frec2uzisod  10421  zfz1isolem1  10834  xrnegiso  11284  reefiso  14551  logltb  14648
  Copyright terms: Public domain W3C validator