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

Definition df-isom 5492
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 5484 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5482 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1652 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1652 . . . . . . 7  class  y
129, 11, 3wbr 4237 . . . . . 6  wff  x R y
139, 5cfv 5483 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5483 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4237 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 178 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2711 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2711 . . 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  6068  isoeq2  6069  isoeq3  6070  isoeq4  6071  isoeq5  6072  nfiso  6073  isof1o  6074  isorel  6075  soisores  6076  soisoi  6077  isoid  6078  isocnv  6079  isocnv2  6080  isocnv3  6081  isores2  6082  isores3  6084  isotr  6085  isoini2  6088  f1oiso  6100  f1owe  6102  smoiso2  6660  alephiso  8010  compssiso  8285  negiso  10015  om2uzisoi  11325  icopnfhmeo  18999  reefiso  20395  logltb  20525  isoun  24120  xrmulc1cn  24347  wepwsolem  27154  iso0  27551
  Copyright terms: Public domain W3C validator