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

Definition df-isom 4609
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 4593 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 4591 . . 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 3920 . . . . . 6  wff  x R y
139, 5cfv 4592 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 4592 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3920 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 178 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2509 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2509 . . 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  5668  isoeq2  5669  isoeq3  5670  isoeq4  5671  isoeq5  5672  nfiso  5673  isof1o  5674  isorel  5675  soisores  5676  soisoi  5677  isoid  5678  isocnv  5679  isocnv2  5680  isocnv3  5681  isores2  5682  isores3  5684  isotr  5685  isoini2  5688  f1oiso  5700  f1owe  5702  smoiso2  6272  alephiso  7609  compssiso  7884  negiso  9610  om2uzisoi  10895  icopnfhmeo  18273  reefiso  19656  logltb  19785  wepwsolem  26304  iso0  26702
  Copyright terms: Public domain W3C validator