Definition df-isom 5505

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 5497	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5495	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1398	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1398	. . . . . . 7 class y
12	9, 11, 3	wbr 4367	. . . . . 6 wff x R y
13	9, 5	cfv 5496	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5496	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4367	. . . . . 6 wff ( H ` x ) S ( H ` y )
16	12, 15	wb 184	. . . . 5 wff ( x R y <-> ( H ` x ) S ( H ` y ) )
17	16, 10, 1	wral 2732	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2732	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 367	. 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 184	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  6116  isoeq2  6117  isoeq3  6118  isoeq4  6119  isoeq5  6120  nfiso  6121  isof1o  6122  isorel  6123  soisores  6124  soisoi  6125  isoid  6126  isocnv  6127  isocnv2  6128  isocnv3  6129  isores2  6130  isores3  6132  isotr  6133  isoini2  6136  f1oiso  6148  f1owe  6150  smoiso2  6958  alephiso  8392  compssiso  8667  negiso  10435  om2uzisoi  11968  icopnfhmeo  21528  reefiso  22928  logltb  23072  isoun  27667  xrmulc1cn  28066  wepwsolem  31153  iso0  31355  fourierdlem54  32109