Definition df-ltxr 5502

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 5498	. 2 class <
2		cltrr 5250	. . . . 5 class <R
3		cr 5245	. . . . . 6 class RR
4	3, 3	cxp 3174	. . . . 5 class (RR X. RR)
5	2, 4	cin 2049	. . . 4 class ( <R i^i (RR X. RR))
6		cmnf 5496	. . . . . 6 class -oo
7		cpnf 5495	. . . . . 6 class +oo
8	6, 7	cop 2415	. . . . 5 class <. -oo, +oo>.
9	8	csn 2413	. . . 4 class {<. -oo, +oo>.}
10	5, 9	cun 2048	. . 3 class (( <R i^i (RR X. RR)) u. {<. -oo, +oo>.})
11	7	csn 2413	. . . . 5 class { +oo}
12	3, 11	cxp 3174	. . . 4 class (RR X. { +oo})
13	6	csn 2413	. . . . 5 class { -oo}
14	13, 3	cxp 3174	. . . 4 class ({ -oo} X. RR)
15	12, 14	cun 2048	. . 3 class ((RR X. { +oo}) u. ({ -oo} X. RR))
16	10, 15	cun 2048	. 2 class ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))
17	1, 16	wceq 958	1 wff < = ((( <R i^i (RR X. RR)) u. {<. -oo, +oo>.}) u. ((RR X. { +oo}) u. ({ -oo} X. RR)))

This definition is referenced by:  ltxrt 5507

Copyright terms: Public domain