New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-iso		GIF version

---

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 ∧ ∀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 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 ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))
18	17, 8, 1	wral 2614	. . 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))))

Colors of variables: wff setvar class

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

Copyright terms: Public domain

W3C validator