Definition df-ltxr 6657

Description: Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. The clipping of <R makes our definition independent of the complex number construction, since the postulates don't presuppose that <R is a relation on RR.

Assertion

Ref	Expression
df-ltxr	|- < = ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))

Detailed syntax breakdown of Definition df-ltxr

Step	Hyp	Ref	Expression
1		clt 6653	. 2 class <
2		cltrr 6390	. . . . 5 class <R
3		cr 6385	. . . . . 6 class RR
4	3, 3	cxp 3984	. . . . 5 class (RR X. RR)
5	2, 4	cin 2592	. . . 4 class ( <R i^i (RR X. RR))
6		cmnf 6651	. . . . . 6 class -oo
7		cpnf 6650	. . . . . 6 class +oo
8	6, 7	cop 3046	. . . . 5 class <. -oo, +oo>.
9	8	csn 3044	. . . 4 class {<. -oo, +oo>.}
10	5, 9	cun 2591	. . 3 class (( <R i^i (RR X. RR)) u. {<. -oo, +oo>.})
11	7	csn 3044	. . . . 5 class { +oo}
12	3, 11	cxp 3984	. . . 4 class (RR X. { +oo})
13	6	csn 3044	. . . . 5 class { -oo}
14	13, 3	cxp 3984	. . . 4 class ({ -oo} X. RR)
15	12, 14	cun 2591	. . 3 class ((RR X. { +oo}) u. ({ -oo} X. RR))
16	10, 15	cun 2591	. 2 class ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))
17	1, 16	wceq 1298	1 wff < = ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))

This definition is referenced by:  ltxr 6664

Copyright terms: Public domain