Definition df-isom 5132

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

Step	Hyp	Ref	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
6	1, 2, 3, 4, 5	wiso 5124	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5122	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1330	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1330	. . . . . . 7 class y
12	9, 11, 3	wbr 3929	. . . . . 6 wff x R y
13	9, 5	cfv 5123	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5123	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 3929	. . . . . 6 wff ( H ` x ) S ( H ` y )
16	12, 15	wb 104	. . . . 5 wff ( x R y <-> ( H ` x ) S ( H ` y ) )
17	16, 10, 1	wral 2416	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2416	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 103	. 2 wff ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) )
20	6, 19	wb 104	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 ) ) ) )

This definition is referenced by:  isoeq1  5702  isoeq2  5703  isoeq3  5704  isoeq4  5705  isoeq5  5706  nfiso  5707  isof1o  5708  isorel  5709  isoid  5711  isocnv  5712  isocnv2  5713  isores2  5714  isores3  5716  isotr  5717  iso0  5718  isoini2  5720  f1oiso  5727  negiso  8713  frec2uzisod  10180  zfz1isolem1  10583  xrnegiso  11031