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

Definition df-isom 5280
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 5272 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5270 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1631 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1631 . . . . . . 7  class  y
129, 11, 3wbr 4039 . . . . . 6  wff  x R y
139, 5cfv 5271 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5271 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4039 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 176 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2556 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2556 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 358 . 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 176 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  5832  isoeq2  5833  isoeq3  5834  isoeq4  5835  isoeq5  5836  nfiso  5837  isof1o  5838  isorel  5839  soisores  5840  soisoi  5841  isoid  5842  isocnv  5843  isocnv2  5844  isocnv3  5845  isores2  5846  isores3  5848  isotr  5849  isoini2  5852  f1oiso  5864  f1owe  5866  smoiso2  6402  alephiso  7741  compssiso  8016  negiso  9746  om2uzisoi  11033  icopnfhmeo  18457  reefiso  19840  logltb  19969  isoun  23257  xrmulc1cn  23318  wepwsolem  27241  iso0  27639
  Copyright terms: Public domain W3C validator