Definition df-isom 5363

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 5355	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5353	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1397	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1397	. . . . . . 7 class y
12	9, 11, 3	wbr 4111	. . . . . 6 wff x R y
13	9, 5	cfv 5354	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5354	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4111	. . . . . 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 2522	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2522	. . 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  5976  isoeq2  5977  isoeq3  5978  isoeq4  5979  isoeq5  5980  nfiso  5981  isof1o  5982  isorel  5983  isoid  5985  isocnv  5986  isocnv2  5987  isores2  5988  isores3  5990  isotr  5991  iso0  5992  isoini2  5994  f1oiso  6001  negiso  9231  frec2uzisod  10773  zfz1isolem1  11216  xrnegiso  11951  reefiso  15659  logltb  15756