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

Definition df-isom 5590
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 5582 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5580 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1373 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1373 . . . . . . 7  class  y
129, 11, 3wbr 4442 . . . . . 6  wff  x R y
139, 5cfv 5581 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5581 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4442 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 184 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2809 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2809 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 369 . 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 184 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 setvar class
This definition is referenced by:  isoeq1  6196  isoeq2  6197  isoeq3  6198  isoeq4  6199  isoeq5  6200  nfiso  6201  isof1o  6202  isorel  6203  soisores  6204  soisoi  6205  isoid  6206  isocnv  6207  isocnv2  6208  isocnv3  6209  isores2  6210  isores3  6212  isotr  6213  isoini2  6216  f1oiso  6228  f1owe  6230  smoiso2  7032  alephiso  8470  compssiso  8745  negiso  10510  om2uzisoi  12023  icopnfhmeo  21173  reefiso  22572  logltb  22707  isoun  27180  xrmulc1cn  27536  wepwsolem  30582  iso0  30781  fourierdlem54  31418
  Copyright terms: Public domain W3C validator