Definition df-ltnqqs 6451

Description: Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)

Assertion

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

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

Detailed syntax breakdown of Definition df-ltnqqs

Step	Hyp	Ref	Expression
1		cltq 6383	. 2 class <Q
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1242	. . . . . 6 class 𝑥
4		cnq 6378	. . . . . 6 class Q
5	3, 4	wcel 1393	. . . . 5 wff 𝑥 ∈ Q
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1242	. . . . . 6 class 𝑦
8	7, 4	wcel 1393	. . . . 5 wff 𝑦 ∈ Q
9	5, 8	wa 97	. . . 4 wff (𝑥 ∈ Q ∧ 𝑦 ∈ Q)
10		vz	. . . . . . . . . . . . . 14 setvar 𝑧
11	10	cv 1242	. . . . . . . . . . . . 13 class 𝑧
12		vw	. . . . . . . . . . . . . 14 setvar 𝑤
13	12	cv 1242	. . . . . . . . . . . . 13 class 𝑤
14	11, 13	cop 3378	. . . . . . . . . . . 12 class ⟨𝑧, 𝑤⟩
15		ceq 6377	. . . . . . . . . . . 12 class ~Q
16	14, 15	cec 6104	. . . . . . . . . . 11 class [⟨𝑧, 𝑤⟩] ~Q
17	3, 16	wceq 1243	. . . . . . . . . 10 wff 𝑥 = [⟨𝑧, 𝑤⟩] ~Q
18		vv	. . . . . . . . . . . . . 14 setvar 𝑣
19	18	cv 1242	. . . . . . . . . . . . 13 class 𝑣
20		vu	. . . . . . . . . . . . . 14 setvar 𝑢
21	20	cv 1242	. . . . . . . . . . . . 13 class 𝑢
22	19, 21	cop 3378	. . . . . . . . . . . 12 class ⟨𝑣, 𝑢⟩
23	22, 15	cec 6104	. . . . . . . . . . 11 class [⟨𝑣, 𝑢⟩] ~Q
24	7, 23	wceq 1243	. . . . . . . . . 10 wff 𝑦 = [⟨𝑣, 𝑢⟩] ~Q
25	17, 24	wa 97	. . . . . . . . 9 wff (𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q )
26		cmi 6372	. . . . . . . . . . 11 class ·N
27	11, 21, 26	co 5512	. . . . . . . . . 10 class (𝑧 ·N 𝑢)
28	13, 19, 26	co 5512	. . . . . . . . . 10 class (𝑤 ·N 𝑣)
29		clti 6373	. . . . . . . . . 10 class <N
30	27, 28, 29	wbr 3764	. . . . . . . . 9 wff (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)
31	25, 30	wa 97	. . . . . . . 8 wff ((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣))
32	31, 20	wex 1381	. . . . . . 7 wff ∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣))
33	32, 18	wex 1381	. . . . . 6 wff ∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣))
34	33, 12	wex 1381	. . . . 5 wff ∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣))
35	34, 10	wex 1381	. . . 4 wff ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣))
36	9, 35	wa 97	. . 3 wff ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))
37	36, 2, 6	copab 3817	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
38	1, 37	wceq 1243	1 wff <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}

This definition is referenced by:  ltrelnq  6463  ordpipqqs  6472