Definition df-isom 5335

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 5327	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5325	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1396	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1396	. . . . . . 7 class y
12	9, 11, 3	wbr 4088	. . . . . 6 wff x R y
13	9, 5	cfv 5326	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5326	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4088	. . . . . 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 2510	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2510	. . 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  5941  isoeq2  5942  isoeq3  5943  isoeq4  5944  isoeq5  5945  nfiso  5946  isof1o  5947  isorel  5948  isoid  5950  isocnv  5951  isocnv2  5952  isores2  5953  isores3  5955  isotr  5956  iso0  5957  isoini2  5959  f1oiso  5966  negiso  9134  frec2uzisod  10668  zfz1isolem1  11103  xrnegiso  11822  reefiso  15500  logltb  15597