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