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

Definition df-isom 5430
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 5422 . 2  wff  H  Isom  R ,  S  ( A ,  B )
71, 2, 5wf1o 5420 . . 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 4180 . . . . . 6  wff  x R y
139, 5cfv 5421 . . . . . . 7  class  ( H `
 x )
1411, 5cfv 5421 . . . . . . 7  class  ( H `
 y )
1513, 14, 4wbr 4180 . . . . . 6  wff  ( H `
 x ) S ( H `  y
)
1612, 15wb 177 . . . . 5  wff  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1716, 10, 1wral 2674 . . . 4  wff  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )
1817, 8, 1wral 2674 . . 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  6006  isoeq2  6007  isoeq3  6008  isoeq4  6009  isoeq5  6010  nfiso  6011  isof1o  6012  isorel  6013  soisores  6014  soisoi  6015  isoid  6016  isocnv  6017  isocnv2  6018  isocnv3  6019  isores2  6020  isores3  6022  isotr  6023  isoini2  6026  f1oiso  6038  f1owe  6040  smoiso2  6598  alephiso  7943  compssiso  8218  negiso  9948  om2uzisoi  11257  icopnfhmeo  18929  reefiso  20325  logltb  20455  isoun  24050  xrmulc1cn  24277  wepwsolem  27014  iso0  27412
  Copyright terms: Public domain W3C validator