Definition df-enq0 6522

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 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}

Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢

Detailed syntax breakdown of Definition df-enq0

Step	Hyp	Ref	Expression
1		ceq0 6384	. 2 class ~Q0
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1242	. . . . . 6 class 𝑥
4		com 4313	. . . . . . 7 class ω
5		cnpi 6370	. . . . . . 7 class N
6	4, 5	cxp 4343	. . . . . 6 class (ω × N)
7	3, 6	wcel 1393	. . . . 5 wff 𝑥 ∈ (ω × N)
8		vy	. . . . . . 7 setvar 𝑦
9	8	cv 1242	. . . . . 6 class 𝑦
10	9, 6	wcel 1393	. . . . 5 wff 𝑦 ∈ (ω × N)
11	7, 10	wa 97	. . . 4 wff (𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N))
12		vz	. . . . . . . . . . . . 13 setvar 𝑧
13	12	cv 1242	. . . . . . . . . . . 12 class 𝑧
14		vw	. . . . . . . . . . . . 13 setvar 𝑤
15	14	cv 1242	. . . . . . . . . . . 12 class 𝑤
16	13, 15	cop 3378	. . . . . . . . . . 11 class ⟨𝑧, 𝑤⟩
17	3, 16	wceq 1243	. . . . . . . . . 10 wff 𝑥 = ⟨𝑧, 𝑤⟩
18		vv	. . . . . . . . . . . . 13 setvar 𝑣
19	18	cv 1242	. . . . . . . . . . . 12 class 𝑣
20		vu	. . . . . . . . . . . . 13 setvar 𝑢
21	20	cv 1242	. . . . . . . . . . . 12 class 𝑢
22	19, 21	cop 3378	. . . . . . . . . . 11 class ⟨𝑣, 𝑢⟩
23	9, 22	wceq 1243	. . . . . . . . . 10 wff 𝑦 = ⟨𝑣, 𝑢⟩
24	17, 23	wa 97	. . . . . . . . 9 wff (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)
25		comu 5999	. . . . . . . . . . 11 class ·𝑜
26	13, 21, 25	co 5512	. . . . . . . . . 10 class (𝑧 ·𝑜 𝑢)
27	15, 19, 25	co 5512	. . . . . . . . . 10 class (𝑤 ·𝑜 𝑣)
28	26, 27	wceq 1243	. . . . . . . . 9 wff (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)
29	24, 28	wa 97	. . . . . . . 8 wff ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
30	29, 20	wex 1381	. . . . . . 7 wff ∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
31	30, 18	wex 1381	. . . . . 6 wff ∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
32	31, 14	wex 1381	. . . . 5 wff ∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
33	32, 12	wex 1381	. . . 4 wff ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
34	11, 33	wa 97	. . 3 wff ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))
35	34, 2, 8	copab 3817	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}
36	1, 35	wceq 1243	1 wff ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}

This definition is referenced by:  enq0enq  6529  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0er  6533  enq0breq  6534  enq0ex  6537