Definition df-iso 2439

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 ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))

Distinct variable group(s):   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 2423	. 2 wff H Isom R, S (A, B)
7	1, 2, 5	wf1o 2421	. . 3 wff H:A–1-1-onto→B
8		vx	. . . . . . . 8 set x
9	8	cv 1089	. . . . . . 7 class x
10		vy	. . . . . . . 8 set y
11	10	cv 1089	. . . . . . 7 class y
12	9, 11, 3	wbr 2054	. . . . . 6 wff xRy
13	9, 5	cfv 2422	. . . . . . 7 class (H ‘x)
14	11, 5	cfv 2422	. . . . . . 7 class (H ‘y)
15	13, 14, 4	wbr 2054	. . . . . 6 wff (H ‘x)S(H ‘y)
16	12, 15	wb 127	. . . . 5 wff (xRy ↔ (H ‘x)S(H ‘y))
17	16, 10, 1	wral 1201	. . . 4 wff ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))
18	17, 8, 1	wral 1201	. . 3 wff ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))
19	7, 18	wa 196	. 2 wff (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y)))
20	6, 19	wb 127	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 2925  isoeq2 2926  isoeq3 2927  isoeq4 2928  isoeq5 2929  hbiso 2930  isof1o 2931  isorel 2932  isoid 2933  isocnv 2934  isotr 2935  isotrALT 2936  f1oiso 2942  f1owe 2943  alephiso 3697

metamath.org