Definition df-isom 5327

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 5319	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5317	. . 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 5318	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5318	. . . . . . 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  5925  isoeq2  5926  isoeq3  5927  isoeq4  5928  isoeq5  5929  nfiso  5930  isof1o  5931  isorel  5932  isoid  5934  isocnv  5935  isocnv2  5936  isores2  5937  isores3  5939  isotr  5940  iso0  5941  isoini2  5943  f1oiso  5950  negiso  9102  frec2uzisod  10629  zfz1isolem1  11062  xrnegiso  11773  reefiso  15451  logltb  15548