# Metamath Proof Explorer

## Definition df-isom

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)

Ref Expression
Assertion 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 ) ) ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cH
` |-  H`
1 cR
` |-  R`
2 cS
` |-  S`
3 cA
` |-  A`
4 cB
` |-  B`
5 3 4 1 2 0 wiso
` |-  H Isom R , S ( A , B )`
6 3 4 0 wf1o
` |-  H : A -1-1-onto-> B`
7 vx
` |-  x`
8 vy
` |-  y`
9 7 cv
` |-  x`
10 8 cv
` |-  y`
11 9 10 1 wbr
` |-  x R y`
12 9 0 cfv
` |-  ( H ` x )`
13 10 0 cfv
` |-  ( H ` y )`
14 12 13 2 wbr
` |-  ( H ` x ) S ( H ` y )`
15 11 14 wb
` |-  ( x R y <-> ( H ` x ) S ( H ` y ) )`
16 15 8 3 wral
` |-  A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )`
17 16 7 3 wral
` |-  A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )`
18 6 17 wa
` |-  ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) )`
19 5 18 wb
` |-  ( 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 ) ) ) )`