This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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