Definition df-isom 5280

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 5272	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5270	. . 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 4044	. . . . . 6 wff x R y
13	9, 5	cfv 5271	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5271	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4044	. . . . . 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  5870  isoeq2  5871  isoeq3  5872  isoeq4  5873  isoeq5  5874  nfiso  5875  isof1o  5876  isorel  5877  isoid  5879  isocnv  5880  isocnv2  5881  isores2  5882  isores3  5884  isotr  5885  iso0  5886  isoini2  5888  f1oiso  5895  negiso  9028  frec2uzisod  10552  zfz1isolem1  10985  xrnegiso  11573  reefiso  15249  logltb  15346