Definition df-isom 5590

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 5582	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5580	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1373	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1373	. . . . . . 7 class y
12	9, 11, 3	wbr 4442	. . . . . 6 wff x R y
13	9, 5	cfv 5581	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5581	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4442	. . . . . 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 2809	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2809	. . 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  6196  isoeq2  6197  isoeq3  6198  isoeq4  6199  isoeq5  6200  nfiso  6201  isof1o  6202  isorel  6203  soisores  6204  soisoi  6205  isoid  6206  isocnv  6207  isocnv2  6208  isocnv3  6209  isores2  6210  isores3  6212  isotr  6213  isoini2  6216  f1oiso  6228  f1owe  6230  smoiso2  7032  alephiso  8470  compssiso  8745  negiso  10510  om2uzisoi  12023  icopnfhmeo  21173  reefiso  22572  logltb  22707  isoun  27180  xrmulc1cn  27536  wepwsolem  30582  iso0  30781  fourierdlem54  31418