Metamath Proof Explorer

Definition df-ltr

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.4 of Gleason p. 127. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-ltr ⊢ < 𝑹 = x y | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltr class < 𝑹
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 cnr class 𝑹
5 3 4 wcel wff x ∈ 𝑹
6 2 cv setvar y
7 6 4 wcel wff y ∈ 𝑹
8 5 7 wa wff x ∈ 𝑹 ∧ y ∈ 𝑹
9 vz setvar z
10 vw setvar w
11 vv setvar v
12 vu setvar u
13 9 cv setvar z
14 10 cv setvar w
15 13 14 cop class z w
16 cer class ~ 𝑹
17 15 16 cec class z w ~ 𝑹
18 3 17 wceq wff x = z w ~ 𝑹
19 11 cv setvar v
20 12 cv setvar u
21 19 20 cop class v u
22 21 16 cec class v u ~ 𝑹
23 6 22 wceq wff y = v u ~ 𝑹
24 18 23 wa wff x = z w ~ 𝑹 ∧ y = v u ~ 𝑹
25 cpp class + 𝑷
26 13 20 25 co class z + 𝑷 u
27 cltp class < 𝑷
28 14 19 25 co class w + 𝑷 v
29 26 28 27 wbr wff z + 𝑷 u < 𝑷 w + 𝑷 v
30 24 29 wa wff x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
31 30 12 wex wff ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
32 31 11 wex wff ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
33 32 10 wex wff ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
34 33 9 wex wff ∃ z ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
35 8 34 wa wff x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
36 35 1 2 copab class x y | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v
37 0 36 wceq wff < 𝑹 = x y | x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ ∃ z ∃ w ∃ v ∃ u x = z w ~ 𝑹 ∧ y = v u ~ 𝑹 ∧ z + 𝑷 u < 𝑷 w + 𝑷 v