Definition df-isom 5281

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 5273	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5271	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1372	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1372	. . . . . . 7 class y
12	9, 11, 3	wbr 4045	. . . . . 6 wff x R y
13	9, 5	cfv 5272	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5272	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4045	. . . . . 6 wff ( H ` x ) S ( H ` y )
16	12, 15	wb 105	. . . . 5 wff ( x R y <-> ( H ` x ) S ( H ` y ) )
17	16, 10, 1	wral 2484	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2484	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 104	. 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 105	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  5872  isoeq2  5873  isoeq3  5874  isoeq4  5875  isoeq5  5876  nfiso  5877  isof1o  5878  isorel  5879  isoid  5881  isocnv  5882  isocnv2  5883  isores2  5884  isores3  5886  isotr  5887  iso0  5888  isoini2  5890  f1oiso  5897  negiso  9030  frec2uzisod  10554  zfz1isolem1  10987  xrnegiso  11606  reefiso  15282  logltb  15379