Definition df-isom 5263

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 5255	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5253	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1363	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1363	. . . . . . 7 class y
12	9, 11, 3	wbr 4029	. . . . . 6 wff x R y
13	9, 5	cfv 5254	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5254	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4029	. . . . . 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 2472	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2472	. . 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  5844  isoeq2  5845  isoeq3  5846  isoeq4  5847  isoeq5  5848  nfiso  5849  isof1o  5850  isorel  5851  isoid  5853  isocnv  5854  isocnv2  5855  isores2  5856  isores3  5858  isotr  5859  iso0  5860  isoini2  5862  f1oiso  5869  negiso  8974  frec2uzisod  10478  zfz1isolem1  10911  xrnegiso  11405  reefiso  14912  logltb  15009