Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ltxr Structured version   Visualization version   GIF version

Definition df-ltxr 10117
 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
StepHypRef Expression
1 clt 10112 . 2 class <
2 vx . . . . . . 7 setvar 𝑥
32cv 1522 . . . . . 6 class 𝑥
4 cr 9973 . . . . . 6 class
53, 4wcel 2030 . . . . 5 wff 𝑥 ∈ ℝ
6 vy . . . . . . 7 setvar 𝑦
76cv 1522 . . . . . 6 class 𝑦
87, 4wcel 2030 . . . . 5 wff 𝑦 ∈ ℝ
9 cltrr 9978 . . . . . 6 class <
103, 7, 9wbr 4685 . . . . 5 wff 𝑥 < 𝑦
115, 8, 10w3a 1054 . . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)
1211, 2, 6copab 4745 . . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)}
13 cmnf 10110 . . . . . . 7 class -∞
1413csn 4210 . . . . . 6 class {-∞}
154, 14cun 3605 . . . . 5 class (ℝ ∪ {-∞})
16 cpnf 10109 . . . . . 6 class +∞
1716csn 4210 . . . . 5 class {+∞}
1815, 17cxp 5141 . . . 4 class ((ℝ ∪ {-∞}) × {+∞})
1914, 4cxp 5141 . . . 4 class ({-∞} × ℝ)
2018, 19cun 3605 . . 3 class (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))
2112, 20cun 3605 . 2 class ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
221, 21wceq 1523 1 wff < = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
 Colors of variables: wff setvar class This definition is referenced by:  ltrelxr  10137  ltxrlt  10146  ltxr  11987
 Copyright terms: Public domain W3C validator