Definition df-isom 5299

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 5291	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5289	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1372	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1372	. . . . . . 7 class y
12	9, 11, 3	wbr 4059	. . . . . 6 wff x R y
13	9, 5	cfv 5290	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5290	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4059	. . . . . 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 2486	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2486	. . 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  5893  isoeq2  5894  isoeq3  5895  isoeq4  5896  isoeq5  5897  nfiso  5898  isof1o  5899  isorel  5900  isoid  5902  isocnv  5903  isocnv2  5904  isores2  5905  isores3  5907  isotr  5908  iso0  5909  isoini2  5911  f1oiso  5918  negiso  9063  frec2uzisod  10589  zfz1isolem1  11022  xrnegiso  11688  reefiso  15364  logltb  15461