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

Definition df-isom 5140
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 5132 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5130 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1331 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1331 . . . . . . 7  class  y
129, 11, 3wbr 3937 . . . . . 6  wff  x R y
139, 5cfv 5131 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5131 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3937 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 104 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2417 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2417 . . 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  5710  isoeq2  5711  isoeq3  5712  isoeq4  5713  isoeq5  5714  nfiso  5715  isof1o  5716  isorel  5717  isoid  5719  isocnv  5720  isocnv2  5721  isores2  5722  isores3  5724  isotr  5725  iso0  5726  isoini2  5728  f1oiso  5735  negiso  8737  frec2uzisod  10211  zfz1isolem1  10615  xrnegiso  11063  reefiso  12906  logltb  13003
  Copyright terms: Public domain W3C validator