Definition df-iso 4797

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 4783	. 2 wff H Isom R, S (A, B)
7	1, 2, 5	wf1o 4781	. . 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 4640	. . . . . 6 wff xRy
13	9, 5	cfv 4782	. . . . . . 7 class (H` x)
14	11, 5	cfv 4782	. . . . . . 7 class (H` y)
15	13, 14, 4	wbr 4640	. . . . . 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 2615	. . . 4 wff A.y e. A (xRy <-> (H` x)S(H` y))
18	17, 8, 1	wral 2615	. . 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  5483  isoeq2  5484  isoeq3  5485  isoeq4  5486  isoeq5  5487  nfiso  5488  isof1o  5489  isorel  5490  isoid  5491  isocnv  5492  isocnv2  5493  isores2  5494  isotr  5496  isoini2  5499  f1oiso  5500