Definition df-isom 5197

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 5189	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5187	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1342	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1342	. . . . . . 7 class y
12	9, 11, 3	wbr 3982	. . . . . 6 wff x R y
13	9, 5	cfv 5188	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5188	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 3982	. . . . . 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 2444	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2444	. . 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  5769  isoeq2  5770  isoeq3  5771  isoeq4  5772  isoeq5  5773  nfiso  5774  isof1o  5775  isorel  5776  isoid  5778  isocnv  5779  isocnv2  5780  isores2  5781  isores3  5783  isotr  5784  iso0  5785  isoini2  5787  f1oiso  5794  negiso  8850  frec2uzisod  10342  zfz1isolem1  10753  xrnegiso  11203  reefiso  13338  logltb  13435