Definition df-isom 5205

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 5197	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5195	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1347	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1347	. . . . . . 7 class y
12	9, 11, 3	wbr 3987	. . . . . 6 wff x R y
13	9, 5	cfv 5196	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5196	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 3987	. . . . . 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 2448	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2448	. . 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  5778  isoeq2  5779  isoeq3  5780  isoeq4  5781  isoeq5  5782  nfiso  5783  isof1o  5784  isorel  5785  isoid  5787  isocnv  5788  isocnv2  5789  isores2  5790  isores3  5792  isotr  5793  iso0  5794  isoini2  5796  f1oiso  5803  negiso  8864  frec2uzisod  10356  zfz1isolem1  10768  xrnegiso  11218  reefiso  13457  logltb  13554