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 ∧ ∀x ∈ A ∀y ∈ 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 ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))
18	17, 8, 1	wral 2615	. . 3 wff ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))
19	7, 18	wa 358	. 2 wff (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ 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 ∧ ∀x ∈ A ∀y ∈ 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