Definition df-isom 5068

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 5060	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5058	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1298	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1298	. . . . . . 7 class y
12	9, 11, 3	wbr 3875	. . . . . 6 wff x R y
13	9, 5	cfv 5059	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5059	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 3875	. . . . . 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 2375	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2375	. . 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  5634  isoeq2  5635  isoeq3  5636  isoeq4  5637  isoeq5  5638  nfiso  5639  isof1o  5640  isorel  5641  isoid  5643  isocnv  5644  isocnv2  5645  isores2  5646  isores3  5648  isotr  5649  iso0  5650  isoini2  5652  f1oiso  5659  negiso  8571  frec2uzisod  10021  zfz1isolem1  10424  xrnegiso  10870