MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-isom Unicode version

Definition df-isom 4655
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 4639 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 4637 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1618 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1618 . . . . . . 7  class  y
129, 11, 3wbr 3963 . . . . . 6  wff  x R y
139, 5cfv 4638 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 4638 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3963 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 178 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2516 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2516 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 360 . 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 178 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  5715  isoeq2  5716  isoeq3  5717  isoeq4  5718  isoeq5  5719  nfiso  5720  isof1o  5721  isorel  5722  soisores  5723  soisoi  5724  isoid  5725  isocnv  5726  isocnv2  5727  isocnv3  5728  isores2  5729  isores3  5731  isotr  5732  isoini2  5735  f1oiso  5747  f1owe  5749  smoiso2  6319  alephiso  7658  compssiso  7933  negiso  9663  om2uzisoi  10948  icopnfhmeo  18368  reefiso  19751  logltb  19880  wepwsolem  26470  iso0  26868
  Copyright terms: Public domain W3C validator