Definition df-isom 5610

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 5602	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5600	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1436	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1436	. . . . . . 7 class y
12	9, 11, 3	wbr 4423	. . . . . 6 wff x R y
13	9, 5	cfv 5601	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5601	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4423	. . . . . 6 wff ( H ` x ) S ( H ` y )
16	12, 15	wb 187	. . . . 5 wff ( x R y <-> ( H ` x ) S ( H ` y ) )
17	16, 10, 1	wral 2771	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2771	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 370	. 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 187	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  6225  isoeq2  6226  isoeq3  6227  isoeq4  6228  isoeq5  6229  nfiso  6230  isof1o  6231  isorel  6232  soisores  6233  soisoi  6234  isoid  6235  isocnv  6236  isocnv2  6237  isocnv3  6238  isores2  6239  isores3  6241  isotr  6242  isoini2  6245  f1oiso  6257  f1owe  6259  smoiso2  7099  alephiso  8536  compssiso  8811  negiso  10594  om2uzisoi  12174  icopnfhmeo  21969  reefiso  23401  logltb  23547  isoun  28284  xrmulc1cn  28744  wepwsolem  35870  iso0  36625  fourierdlem54  37964