Definition df-iso 3199

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.

Assertion

Ref	Expression
df-iso	|- (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (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-iso

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 3183	. 2 wff H Isom R, S (A, B)
7	1, 2, 5	wf1o 3181	. . 3 wff H:A-1-1-onto->B
8		vx	. . . . . . . 8 set x
9	8	cv 955	. . . . . . 7 class x
10		vy	. . . . . . . 8 set y
11	10	cv 955	. . . . . . 7 class y
12	9, 11, 3	wbr 2619	. . . . . 6 wff xRy
13	9, 5	cfv 3182	. . . . . . 7 class (H` x)
14	11, 5	cfv 3182	. . . . . . 7 class (H` y)
15	13, 14, 4	wbr 2619	. . . . . 6 wff (H` x)S(H` y)
16	12, 15	wb 146	. . . . 5 wff (xRy <-> (H` x)S(H` y))
17	16, 10, 1	wral 1645	. . . 4 wff A.y e. A (xRy <-> (H` x)S(H` y))
18	17, 8, 1	wral 1645	. . 3 wff A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))
19	7, 18	wa 223	. 2 wff (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y)))
20	6, 19	wb 146	1 wff (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))

This definition is referenced by:  isoeq1 3887  isoeq2 3888  isoeq3 3889  isoeq4 3890  isoeq5 3891  hbiso 3892  isof1o 3893  isorel 3894  isoid 3895  isocnv 3896  isotr 3897  isotrALT 3898  f1oiso 3904  f1owe 3905  alephiso 4892  reefiso 7428  logltbt 8776

Copyright terms: Public domain