Definition df-isom 5330

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 5322	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5320	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1394	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1394	. . . . . . 7 class y
12	9, 11, 3	wbr 4083	. . . . . 6 wff x R y
13	9, 5	cfv 5321	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5321	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4083	. . . . . 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 2508	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2508	. . 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  5934  isoeq2  5935  isoeq3  5936  isoeq4  5937  isoeq5  5938  nfiso  5939  isof1o  5940  isorel  5941  isoid  5943  isocnv  5944  isocnv2  5945  isores2  5946  isores3  5948  isotr  5949  iso0  5950  isoini2  5952  f1oiso  5959  negiso  9118  frec2uzisod  10646  zfz1isolem1  11080  xrnegiso  11794  reefiso  15472  logltb  15569