Definition df-ltnqqs 6206

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 = {⟨x, y⟩ ∣ ((x ∈ Q ∧ y ∈ Q) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩] ~Q ∧ y = [⟨v, u⟩] ~Q ) ∧ (z ·N u) <N (w ·N v)))}

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

Detailed syntax breakdown of Definition df-ltnqqs

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

This definition is referenced by:  ltrelnq  6218  ordpipqqs  6227