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	⊢ < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clt	⊢ <
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cr	⊢ ℝ
5	3 4	wcel	⊢ 𝑥 ∈ ℝ
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ ℝ
8		cltrr	⊢ <ℝ
9	3 6 8	wbr	⊢ 𝑥 <ℝ 𝑦
10	5 7 9	w3a	⊢ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 )
11	10 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) }
12		cmnf	⊢ -∞
13	12	csn	⊢ { -∞ }
14	4 13	cun	⊢ ( ℝ ∪ { -∞ } )
15		cpnf	⊢ +∞
16	15	csn	⊢ { +∞ }
17	14 16	cxp	⊢ ( ( ℝ ∪ { -∞ } ) × { +∞ } )
18	13 4	cxp	⊢ ( { -∞ } × ℝ )
19	17 18	cun	⊢ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) )
20	11 19	cun	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )
21	0 20	wceq	⊢ < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )