Definition df-ltxr 7065

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

Step	Hyp	Ref	Expression
1		clt 7060	. 2 class <
2		vx	. . . . . . 7 setvar x
3	2	cv 1242	. . . . . 6 class x
4		cr 6888	. . . . . 6 class RR
5	3, 4	wcel 1393	. . . . 5 wff x e. RR
6		vy	. . . . . . 7 setvar y
7	6	cv 1242	. . . . . 6 class y
8	7, 4	wcel 1393	. . . . 5 wff y e. RR
9		cltrr 6893	. . . . . 6 class <RR
10	3, 7, 9	wbr 3764	. . . . 5 wff x <RR y
11	5, 8, 10	w3a 885	. . . 4 wff ( x e. RR /\ y e. RR /\ x <RR y )
12	11, 2, 6	copab 3817	. . 3 class { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) }
13		cmnf 7058	. . . . . . 7 class -oo
14	13	csn 3375	. . . . . 6 class { -oo }
15	4, 14	cun 2915	. . . . 5 class ( RR u. { -oo } )
16		cpnf 7057	. . . . . 6 class +oo
17	16	csn 3375	. . . . 5 class { +oo }
18	15, 17	cxp 4343	. . . 4 class ( ( RR u. { -oo } ) X. { +oo } )
19	14, 4	cxp 4343	. . . 4 class ( { -oo } X. RR )
20	18, 19	cun 2915	. . 3 class ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) )
21	12, 20	cun 2915	. 2 class ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )
22	1, 21	wceq 1243	1 wff < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x <RR y ) } u. ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) )

This definition is referenced by:  ltrelxr  7080  ltxrlt  7085  ltxr  8695