Definition df-iso 4796

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 SF, 5-Jan-2015.)

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 4782	. 2 wff H Isom R, S (A, B)
7	1, 2, 5	wf1o 4780	. . 3 wff H:A-1-1-onto->B
8		vx	. . . . . . . 8 setvar x
9	8	cv 1641	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1641	. . . . . . 7 class y
12	9, 11, 3	wbr 4639	. . . . . 6 wff xRy
13	9, 5	cfv 4781	. . . . . . 7 class (H` x)
14	11, 5	cfv 4781	. . . . . . 7 class (H` y)
15	13, 14, 4	wbr 4639	. . . . . 6 wff (H` x)S(H` y)
16	12, 15	wb 176	. . . . 5 wff (xRy <-> (H` x)S(H` y))
17	16, 10, 1	wral 2614	. . . 4 wff A.y e. A (xRy <-> (H` x)S(H` y))
18	17, 8, 1	wral 2614	. . 3 wff A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))
19	7, 18	wa 358	. 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 176	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  5482  isoeq2  5483  isoeq3  5484  isoeq4  5485  isoeq5  5486  nfiso  5487  isof1o  5488  isorel  5489  isoid  5490  isocnv  5491  isocnv2  5492  isores2  5493  isotr  5495  isoini2  5498  f1oiso  5499