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

Definition df-isom 5422
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 5414 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5412 . . 3  wff  H : A
-1-1-onto-> B
8 vx . . . . . . . 8  set  x
98cv 1648 . . . . . . 7  class  x
10 vy . . . . . . . 8  set  y
1110cv 1648 . . . . . . 7  class  y
129, 11, 3wbr 4172 . . . . . 6  wff  x R y
139, 5cfv 5413 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5413 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4172 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 177 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2666 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2666 . . 3  wff  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
197, 18wa 359 . 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 177 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  5998  isoeq2  5999  isoeq3  6000  isoeq4  6001  isoeq5  6002  nfiso  6003  isof1o  6004  isorel  6005  soisores  6006  soisoi  6007  isoid  6008  isocnv  6009  isocnv2  6010  isocnv3  6011  isores2  6012  isores3  6014  isotr  6015  isoini2  6018  f1oiso  6030  f1owe  6032  smoiso2  6590  alephiso  7935  compssiso  8210  negiso  9940  om2uzisoi  11249  icopnfhmeo  18921  reefiso  20317  logltb  20447  isoun  24042  xrmulc1cn  24269  wepwsolem  27006  iso0  27404
  Copyright terms: Public domain W3C validator