ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ltxr Structured version   GIF version

Definition df-ltxr 6822
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 < = ({⟨x, y⟩ ∣ (x y x < y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-ltxr
StepHypRef Expression
1 clt 6817 . 2 class <
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cr 6670 . . . . . 6 class
53, 4wcel 1390 . . . . 5 wff x
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y
9 cltrr 6675 . . . . . 6 class <
103, 7, 9wbr 3755 . . . . 5 wff x < y
115, 8, 10w3a 884 . . . 4 wff (x y x < y)
1211, 2, 6copab 3808 . . 3 class {⟨x, y⟩ ∣ (x y x < y)}
13 cmnf 6815 . . . . . . 7 class -∞
1413csn 3367 . . . . . 6 class {-∞}
154, 14cun 2909 . . . . 5 class (ℝ ∪ {-∞})
16 cpnf 6814 . . . . . 6 class +∞
1716csn 3367 . . . . 5 class {+∞}
1815, 17cxp 4286 . . . 4 class ((ℝ ∪ {-∞}) × {+∞})
1914, 4cxp 4286 . . . 4 class ({-∞} × ℝ)
2018, 19cun 2909 . . 3 class (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))
2112, 20cun 2909 . 2 class ({⟨x, y⟩ ∣ (x y x < y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
221, 21wceq 1242 1 wff < = ({⟨x, y⟩ ∣ (x y x < y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
Colors of variables: wff set class
This definition is referenced by:  ltrelxr  6837  ltxrlt  6842  ltxr  8425
  Copyright terms: Public domain W3C validator