Definition df-enq 6200

Description: Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.)

Assertion

Ref	Expression
df-enq	⊢ ~Q = {⟨x, y⟩ ∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v)))}

Distinct variable group:   x,y,z,w,v,u

Detailed syntax breakdown of Definition df-enq

Step	Hyp	Ref	Expression
1		ceq 6133	. 2 class ~Q
2		vx	. . . . . . 7 setvar x
3	2	cv 1225	. . . . . 6 class x
4		cnpi 6126	. . . . . . 7 class N
5	4, 4	cxp 4266	. . . . . 6 class (N × N)
6	3, 5	wcel 1370	. . . . 5 wff x ∈ (N × N)
7		vy	. . . . . . 7 setvar y
8	7	cv 1225	. . . . . 6 class y
9	8, 5	wcel 1370	. . . . 5 wff y ∈ (N × N)
10	6, 9	wa 97	. . . 4 wff (x ∈ (N × N) ∧ y ∈ (N × N))
11		vz	. . . . . . . . . . . . 13 setvar z
12	11	cv 1225	. . . . . . . . . . . 12 class z
13		vw	. . . . . . . . . . . . 13 setvar w
14	13	cv 1225	. . . . . . . . . . . 12 class w
15	12, 14	cop 3349	. . . . . . . . . . 11 class ⟨z, w⟩
16	3, 15	wceq 1226	. . . . . . . . . 10 wff x = ⟨z, w⟩
17		vv	. . . . . . . . . . . . 13 setvar v
18	17	cv 1225	. . . . . . . . . . . 12 class v
19		vu	. . . . . . . . . . . . 13 setvar u
20	19	cv 1225	. . . . . . . . . . . 12 class u
21	18, 20	cop 3349	. . . . . . . . . . 11 class ⟨v, u⟩
22	8, 21	wceq 1226	. . . . . . . . . 10 wff y = ⟨v, u⟩
23	16, 22	wa 97	. . . . . . . . 9 wff (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)
24		cmi 6128	. . . . . . . . . . 11 class ·N
25	12, 20, 24	co 5432	. . . . . . . . . 10 class (z ·N u)
26	14, 18, 24	co 5432	. . . . . . . . . 10 class (w ·N v)
27	25, 26	wceq 1226	. . . . . . . . 9 wff (z ·N u) = (w ·N v)
28	23, 27	wa 97	. . . . . . . 8 wff ((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v))
29	28, 19	wex 1358	. . . . . . 7 wff ∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v))
30	29, 17	wex 1358	. . . . . 6 wff ∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v))
31	30, 13	wex 1358	. . . . 5 wff ∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v))
32	31, 11	wex 1358	. . . 4 wff ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v))
33	10, 32	wa 97	. . 3 wff ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v)))
34	33, 2, 7	copab 3787	. 2 class {⟨x, y⟩ ∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v)))}
35	1, 34	wceq 1226	1 wff ~Q = {⟨x, y⟩ ∣ ((x ∈ (N × N) ∧ y ∈ (N × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·N u) = (w ·N v)))}

This definition is referenced by:  enqbreq  6209  enqer  6211  enqex  6213  addpipqqs  6223  mulpipqqs  6226  enq0enq  6280