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

Definition df-ltxr 9127
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  |-  <  =  ( { <. x ,  y
>.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-ltxr
StepHypRef Expression
1 clt 9122 . 2  class  <
2 vx . . . . . . 7  set  x
32cv 1652 . . . . . 6  class  x
4 cr 8991 . . . . . 6  class  RR
53, 4wcel 1726 . . . . 5  wff  x  e.  RR
6 vy . . . . . . 7  set  y
76cv 1652 . . . . . 6  class  y
87, 4wcel 1726 . . . . 5  wff  y  e.  RR
9 cltrr 8996 . . . . . 6  class  <RR
103, 7, 9wbr 4214 . . . . 5  wff  x  <RR  y
115, 8, 10w3a 937 . . . 4  wff  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y )
1211, 2, 6copab 4267 . . 3  class  { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }
13 cmnf 9120 . . . . . . 7  class  -oo
1413csn 3816 . . . . . 6  class  {  -oo }
154, 14cun 3320 . . . . 5  class  ( RR  u.  {  -oo }
)
16 cpnf 9119 . . . . . 6  class  +oo
1716csn 3816 . . . . 5  class  {  +oo }
1815, 17cxp 4878 . . . 4  class  ( ( RR  u.  {  -oo } )  X.  {  +oo } )
1914, 4cxp 4878 . . . 4  class  ( { 
-oo }  X.  RR )
2018, 19cun 3320 . . 3  class  ( ( ( RR  u.  {  -oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) )
2112, 20cun 3320 . 2  class  ( {
<. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
221, 21wceq 1653 1  wff  <  =  ( { <. x ,  y
>.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { 
-oo } )  X.  {  +oo } )  u.  ( {  -oo }  X.  RR ) ) )
Colors of variables: wff set class
This definition is referenced by:  ltrelxr  9141  ltxrlt  9148  ltxr  10717
  Copyright terms: Public domain W3C validator