Metamath Proof Explorer

Definition df-ltxr

Description: Define 'less than' on the set of extended reals. Definition 12-3.1 of Gleason p. 173. Note that in our postulates for complex numbers, is primitive and not necessarily a relation on RR . (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion df-ltxr ⊢ < = x y | x ∈ ℝ ∧ y ∈ ℝ ∧ x < ℝ y ∪ ℝ ∪ −∞ × +∞ ∪ −∞ × ℝ

Detailed syntax breakdown

Step Hyp Ref Expression
0 clt class <
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 cr class ℝ
5 3 4 wcel wff x ∈ ℝ
6 2 cv setvar y
7 6 4 wcel wff y ∈ ℝ
8 cltrr class < ℝ
9 3 6 8 wbr wff x < ℝ y
10 5 7 9 w3a wff x ∈ ℝ ∧ y ∈ ℝ ∧ x < ℝ y
11 10 1 2 copab class x y | x ∈ ℝ ∧ y ∈ ℝ ∧ x < ℝ y
12 cmnf class −∞
13 12 csn class −∞
14 4 13 cun class ℝ ∪ −∞
15 cpnf class +∞
16 15 csn class +∞
17 14 16 cxp class ℝ ∪ −∞ × +∞
18 13 4 cxp class −∞ × ℝ
19 17 18 cun class ℝ ∪ −∞ × +∞ ∪ −∞ × ℝ
20 11 19 cun class x y | x ∈ ℝ ∧ y ∈ ℝ ∧ x < ℝ y ∪ ℝ ∪ −∞ × +∞ ∪ −∞ × ℝ
21 0 20 wceq wff < = x y | x ∈ ℝ ∧ y ∈ ℝ ∧ x < ℝ y ∪ ℝ ∪ −∞ × +∞ ∪ −∞ × ℝ