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

Definition df-isom 5230
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 5222 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5220 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1627 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1627 . . . . . . 7  class  y
129, 11, 3wbr 4024 . . . . . 6  wff  x R y
139, 5cfv 5221 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5221 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4024 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 178 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2544 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2544 . . 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  5777  isoeq2  5778  isoeq3  5779  isoeq4  5780  isoeq5  5781  nfiso  5782  isof1o  5783  isorel  5784  soisores  5785  soisoi  5786  isoid  5787  isocnv  5788  isocnv2  5789  isocnv3  5790  isores2  5791  isores3  5793  isotr  5794  isoini2  5797  f1oiso  5809  f1owe  5811  smoiso2  6381  alephiso  7720  compssiso  7995  negiso  9725  om2uzisoi  11011  icopnfhmeo  18435  reefiso  19818  logltb  19947  wepwsolem  26537  iso0  26935
  Copyright terms: Public domain W3C validator