Definition df-isom 5587

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 5579	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5577	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1382	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1382	. . . . . . 7 class y
12	9, 11, 3	wbr 4437	. . . . . 6 wff x R y
13	9, 5	cfv 5578	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5578	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4437	. . . . . 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 2793	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2793	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 369	. 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  6200  isoeq2  6201  isoeq3  6202  isoeq4  6203  isoeq5  6204  nfiso  6205  isof1o  6206  isorel  6207  soisores  6208  soisoi  6209  isoid  6210  isocnv  6211  isocnv2  6212  isocnv3  6213  isores2  6214  isores3  6216  isotr  6217  isoini2  6220  f1oiso  6232  f1owe  6234  smoiso2  7042  alephiso  8482  compssiso  8757  negiso  10526  om2uzisoi  12047  icopnfhmeo  21421  reefiso  22821  logltb  22962  isoun  27498  xrmulc1cn  27890  wepwsolem  30963  iso0  31163  fourierdlem54  31897