This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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