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 ) ) ) )