Definition df-isom 5384

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 5376	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5374	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1401	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1401	. . . . . . 7 class y
12	9, 11, 3	wbr 4128	. . . . . 6 wff x R y
13	9, 5	cfv 5375	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5375	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4128	. . . . . 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 2528	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2528	. . 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  6000  isoeq2  6001  isoeq3  6002  isoeq4  6003  isoeq5  6004  nfiso  6005  isof1o  6006  isorel  6007  isoid  6009  isocnv  6010  isocnv2  6011  isores2  6012  isores3  6014  isotr  6015  iso0  6016  isoini2  6018  f1oiso  6025  negiso  9278  frec2uzisod  10825  zfz1isolem1  11273  xrnegiso  12009  reefiso  15804  logltb  15901