Definition df-ltxr 10920

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 ℝ. (Contributed by NM, 13-Oct-2005.)

Assertion

Ref	Expression
df-ltxr	⊢ < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ltxr

Step	Hyp	Ref	Expression
1		clt 10915	. 2 class <
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1542	. . . . . 6 class 𝑥
4		cr 10776	. . . . . 6 class ℝ
5	3, 4	wcel 2112	. . . . 5 wff 𝑥 ∈ ℝ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1542	. . . . . 6 class 𝑦
8	7, 4	wcel 2112	. . . . 5 wff 𝑦 ∈ ℝ
9		cltrr 10781	. . . . . 6 class <ℝ
10	3, 7, 9	wbr 5070	. . . . 5 wff 𝑥 <ℝ 𝑦
11	5, 8, 10	w3a 1089	. . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)
12	11, 2, 6	copab 5132	. . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}
13		cmnf 10913	. . . . . . 7 class -∞
14	13	csn 4558	. . . . . 6 class {-∞}
15	4, 14	cun 3882	. . . . 5 class (ℝ ∪ {-∞})
16		cpnf 10912	. . . . . 6 class +∞
17	16	csn 4558	. . . . 5 class {+∞}
18	15, 17	cxp 5577	. . . 4 class ((ℝ ∪ {-∞}) × {+∞})
19	14, 4	cxp 5577	. . . 4 class ({-∞} × ℝ)
20	18, 19	cun 3882	. . 3 class (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))
21	12, 20	cun 3882	. 2 class ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
22	1, 21	wceq 1543	1 wff < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))

This definition is referenced by:  ltrelxr  10942  ltxrlt  10951  ltxr  12755