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

Definition df-isom 4676
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 4660 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 4658 . . 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 3983 . . . . . 6  wff  x R y
139, 5cfv 4659 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 4659 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 3983 . . . . . 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  5736  isoeq2  5737  isoeq3  5738  isoeq4  5739  isoeq5  5740  nfiso  5741  isof1o  5742  isorel  5743  soisores  5744  soisoi  5745  isoid  5746  isocnv  5747  isocnv2  5748  isocnv3  5749  isores2  5750  isores3  5752  isotr  5753  isoini2  5756  f1oiso  5768  f1owe  5770  smoiso2  6340  alephiso  7679  compssiso  7954  negiso  9684  om2uzisoi  10969  icopnfhmeo  18389  reefiso  19772  logltb  19901  wepwsolem  26491  iso0  26889
  Copyright terms: Public domain W3C validator