Definition df-isom 5225

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 5217	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5215	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1352	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1352	. . . . . . 7 class y
12	9, 11, 3	wbr 4003	. . . . . 6 wff x R y
13	9, 5	cfv 5216	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5216	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4003	. . . . . 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 2455	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2455	. . 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  5801  isoeq2  5802  isoeq3  5803  isoeq4  5804  isoeq5  5805  nfiso  5806  isof1o  5807  isorel  5808  isoid  5810  isocnv  5811  isocnv2  5812  isores2  5813  isores3  5815  isotr  5816  iso0  5817  isoini2  5819  f1oiso  5826  negiso  8911  frec2uzisod  10406  zfz1isolem1  10819  xrnegiso  11269  reefiso  14168  logltb  14265