Definition df-enq0 6406

Description: Define equivalence relation for non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)

Assertion

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

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

Detailed syntax breakdown of Definition df-enq0

Step	Hyp	Ref	Expression
1		ceq0 6270	. 2 class ~Q0
2		vx	. . . . . . 7 setvar x
3	2	cv 1241	. . . . . 6 class x
4		com 4256	. . . . . . 7 class 𝜔
5		cnpi 6256	. . . . . . 7 class N
6	4, 5	cxp 4286	. . . . . 6 class (𝜔 × N)
7	3, 6	wcel 1390	. . . . 5 wff x ∈ (𝜔 × N)
8		vy	. . . . . . 7 setvar y
9	8	cv 1241	. . . . . 6 class y
10	9, 6	wcel 1390	. . . . 5 wff y ∈ (𝜔 × N)
11	7, 10	wa 97	. . . 4 wff (x ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N))
12		vz	. . . . . . . . . . . . 13 setvar z
13	12	cv 1241	. . . . . . . . . . . 12 class z
14		vw	. . . . . . . . . . . . 13 setvar w
15	14	cv 1241	. . . . . . . . . . . 12 class w
16	13, 15	cop 3370	. . . . . . . . . . 11 class ⟨z, w⟩
17	3, 16	wceq 1242	. . . . . . . . . 10 wff x = ⟨z, w⟩
18		vv	. . . . . . . . . . . . 13 setvar v
19	18	cv 1241	. . . . . . . . . . . 12 class v
20		vu	. . . . . . . . . . . . 13 setvar u
21	20	cv 1241	. . . . . . . . . . . 12 class u
22	19, 21	cop 3370	. . . . . . . . . . 11 class ⟨v, u⟩
23	9, 22	wceq 1242	. . . . . . . . . 10 wff y = ⟨v, u⟩
24	17, 23	wa 97	. . . . . . . . 9 wff (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)
25		comu 5938	. . . . . . . . . . 11 class ·𝑜
26	13, 21, 25	co 5455	. . . . . . . . . 10 class (z ·𝑜 u)
27	15, 19, 25	co 5455	. . . . . . . . . 10 class (w ·𝑜 v)
28	26, 27	wceq 1242	. . . . . . . . 9 wff (z ·𝑜 u) = (w ·𝑜 v)
29	24, 28	wa 97	. . . . . . . 8 wff ((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v))
30	29, 20	wex 1378	. . . . . . 7 wff ∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v))
31	30, 18	wex 1378	. . . . . 6 wff ∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v))
32	31, 14	wex 1378	. . . . 5 wff ∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v))
33	32, 12	wex 1378	. . . 4 wff ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v))
34	11, 33	wa 97	. . 3 wff ((x ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v)))
35	34, 2, 8	copab 3808	. 2 class {⟨x, y⟩ ∣ ((x ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v)))}
36	1, 35	wceq 1242	1 wff ~Q0 = {⟨x, y⟩ ∣ ((x ∈ (𝜔 × N) ∧ y ∈ (𝜔 × N)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (z ·𝑜 u) = (w ·𝑜 v)))}

This definition is referenced by:  enq0enq  6413  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0er  6417  enq0breq  6418  enq0ex  6421