Definition df-isom 5191

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 5183	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5181	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1341	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1341	. . . . . . 7 class y
12	9, 11, 3	wbr 3976	. . . . . 6 wff x R y
13	9, 5	cfv 5182	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5182	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 3976	. . . . . 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 2442	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2442	. . 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  5763  isoeq2  5764  isoeq3  5765  isoeq4  5766  isoeq5  5767  nfiso  5768  isof1o  5769  isorel  5770  isoid  5772  isocnv  5773  isocnv2  5774  isores2  5775  isores3  5777  isotr  5778  iso0  5779  isoini2  5781  f1oiso  5788  negiso  8841  frec2uzisod  10332  zfz1isolem1  10739  xrnegiso  11189  reefiso  13239  logltb  13336