Definition df-enq 10902

Description: Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11112, 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.) (New usage is discouraged.)

Assertion

Ref	Expression
df-enq	⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}

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

Detailed syntax breakdown of Definition df-enq

Step	Hyp	Ref	Expression
1		ceq 10842	. 2 class ~Q
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1541	. . . . . 6 class 𝑥
4		cnpi 10835	. . . . . . 7 class N
5	4, 4	cxp 5673	. . . . . 6 class (N × N)
6	3, 5	wcel 2107	. . . . 5 wff 𝑥 ∈ (N × N)
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1541	. . . . . 6 class 𝑦
9	8, 5	wcel 2107	. . . . 5 wff 𝑦 ∈ (N × N)
10	6, 9	wa 397	. . . 4 wff (𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N))
11		vz	. . . . . . . . . . . . 13 setvar 𝑧
12	11	cv 1541	. . . . . . . . . . . 12 class 𝑧
13		vw	. . . . . . . . . . . . 13 setvar 𝑤
14	13	cv 1541	. . . . . . . . . . . 12 class 𝑤
15	12, 14	cop 4633	. . . . . . . . . . 11 class ⟨𝑧, 𝑤⟩
16	3, 15	wceq 1542	. . . . . . . . . 10 wff 𝑥 = ⟨𝑧, 𝑤⟩
17		vv	. . . . . . . . . . . . 13 setvar 𝑣
18	17	cv 1541	. . . . . . . . . . . 12 class 𝑣
19		vu	. . . . . . . . . . . . 13 setvar 𝑢
20	19	cv 1541	. . . . . . . . . . . 12 class 𝑢
21	18, 20	cop 4633	. . . . . . . . . . 11 class ⟨𝑣, 𝑢⟩
22	8, 21	wceq 1542	. . . . . . . . . 10 wff 𝑦 = ⟨𝑣, 𝑢⟩
23	16, 22	wa 397	. . . . . . . . 9 wff (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)
24		cmi 10837	. . . . . . . . . . 11 class ·N
25	12, 20, 24	co 7404	. . . . . . . . . 10 class (𝑧 ·N 𝑢)
26	14, 18, 24	co 7404	. . . . . . . . . 10 class (𝑤 ·N 𝑣)
27	25, 26	wceq 1542	. . . . . . . . 9 wff (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)
28	23, 27	wa 397	. . . . . . . 8 wff ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))
29	28, 19	wex 1782	. . . . . . 7 wff ∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))
30	29, 17	wex 1782	. . . . . 6 wff ∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))
31	30, 13	wex 1782	. . . . 5 wff ∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))
32	31, 11	wex 1782	. . . 4 wff ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣))
33	10, 32	wa 397	. . 3 wff ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))
34	33, 2, 7	copab 5209	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
35	1, 34	wceq 1542	1 wff ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}

This definition is referenced by:  enqbreq  10910  enqer  10912  enqex  10913