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

Definition df-isom 5610
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 5602 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5600 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  setvar  x
98cv 1454 . . . . . . 7  class  x
10 vy . . . . . . . 8  setvar  y
1110cv 1454 . . . . . . 7  class  y
129, 11, 3wbr 4416 . . . . . 6  wff  x R y
139, 5cfv 5601 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5601 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4416 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 189 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2749 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2749 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 375 . 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 189 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  6235  isoeq2  6236  isoeq3  6237  isoeq4  6238  isoeq5  6239  nfiso  6240  isof1o  6241  isorel  6242  soisores  6243  soisoi  6244  isoid  6245  isocnv  6246  isocnv2  6247  isocnv3  6248  isores2  6249  isores3  6251  isotr  6252  isoini2  6255  f1oiso  6267  f1owe  6269  smoiso2  7114  alephiso  8555  compssiso  8830  negiso  10615  om2uzisoi  12200  icopnfhmeo  22020  reefiso  23452  logltb  23598  isoun  28331  xrmulc1cn  28785  wepwsolem  35945  iso0  36699  fourierdlem54  38062
  Copyright terms: Public domain W3C validator