Definition df-isom 5237

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 5229	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5227	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1362	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1362	. . . . . . 7 class y
12	9, 11, 3	wbr 4015	. . . . . 6 wff x R y
13	9, 5	cfv 5228	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5228	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4015	. . . . . 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 2465	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2465	. . 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  5815  isoeq2  5816  isoeq3  5817  isoeq4  5818  isoeq5  5819  nfiso  5820  isof1o  5821  isorel  5822  isoid  5824  isocnv  5825  isocnv2  5826  isores2  5827  isores3  5829  isotr  5830  iso0  5831  isoini2  5833  f1oiso  5840  negiso  8926  frec2uzisod  10421  zfz1isolem1  10834  xrnegiso  11284  reefiso  14551  logltb  14648