Metamath Proof Explorer

Definition df-ltxr

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

Ref Expression
Assertion df-ltxr 
|- < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clt 
 |-  <
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 cr 
 |-  RR
5 3 4 wcel 
 |-  x e. RR
6 2 cv 
 |-  y
7 6 4 wcel 
 |-  y e. RR
8 cltrr 
 |-
9 3 6 8 wbr 
 |-  x
10 5 7 9 w3a 
 |-  ( x e. RR /\ y e. RR /\ x
11 10 1 2 copab 
 |-  { <. x , y >. | ( x e. RR /\ y e. RR /\ x
12 cmnf 
 |-  -oo
13 12 csn 
 |-  { -oo }
14 4 13 cun 
 |-  ( RR u. { -oo } )
15 cpnf 
 |-  +oo
16 15 csn 
 |-  { +oo }
17 14 16 cxp 
 |-  ( ( RR u. { -oo } ) X. { +oo } )
18 13 4 cxp 
 |-  ( { -oo } X. RR )
19 17 18 cun 
 |-  ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) )
20 11 19 cun 
 |-  ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x
21 0 20 wceq 
 |-  < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x