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

Definition df-ltxr 6862
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,  <RR is primitive and not necessarily a relation on  RR. (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
df-ltxr  <  { <. , 
>.  |  RR  RR  <RR  }  u.  RR  u.  { -oo }  X.  { +oo }  u.  { -oo }  X.  RR
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ltxr
StepHypRef Expression
1 clt 6857 . 2  <
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cr 6710 . . . . . 6  RR
53, 4wcel 1390 . . . . 5  RR
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5  RR
9 cltrr 6715 . . . . . 6  <RR
103, 7, 9wbr 3755 . . . . 5  <RR
115, 8, 10w3a 884 . . . 4  RR  RR  <RR
1211, 2, 6copab 3808 . . 3  { <. ,  >.  |  RR  RR  <RR  }
13 cmnf 6855 . . . . . . 7 -oo
1413csn 3367 . . . . . 6  { -oo }
154, 14cun 2909 . . . . 5  RR  u.  { -oo }
16 cpnf 6854 . . . . . 6 +oo
1716csn 3367 . . . . 5  { +oo }
1815, 17cxp 4286 . . . 4  RR  u.  { -oo }  X.  { +oo }
1914, 4cxp 4286 . . . 4  { -oo }  X.  RR
2018, 19cun 2909 . . 3  RR  u.  { -oo }  X.  { +oo }  u.  { -oo }  X.  RR
2112, 20cun 2909 . 2  { <. ,  >.  |  RR  RR  <RR  }  u.  RR  u.  { -oo }  X.  { +oo }  u.  { -oo }  X.  RR
221, 21wceq 1242 1  <  { <. ,  >.  |  RR  RR  <RR  }  u.  RR  u.  { -oo }  X.  { +oo }  u.  { -oo }  X.  RR
Colors of variables: wff set class
This definition is referenced by:  ltrelxr  6877  ltxrlt  6882  ltxr  8465
  Copyright terms: Public domain W3C validator