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

Metamath Proof Explorer

Theorem ltrelxr

Description: "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion ltrelxr < ⊆ ( ℝ* × ℝ* )

Proof

Step Hyp Ref Expression
1 df-ltxr ⊢ < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )
2 df-3an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) )
3 2 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) }
4 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) } ⊆ ( ℝ × ℝ )
5 3 4 eqsstri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ⊆ ( ℝ × ℝ )
6 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
7 5 6 sstri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ⊆ ( ℝ* × ℝ* )
8 ressxr ⊢ ℝ ⊆ ℝ*
9 snsspr2 ⊢ { -∞ } ⊆ { +∞ , -∞ }
10 ssun2 ⊢ { +∞ , -∞ } ⊆ ( ℝ ∪ { +∞ , -∞ } )
11 df-xr ⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
12 10 11 sseqtrri ⊢ { +∞ , -∞ } ⊆ ℝ*
13 9 12 sstri ⊢ { -∞ } ⊆ ℝ*
14 8 13 unssi ⊢ ( ℝ ∪ { -∞ } ) ⊆ ℝ*
15 snsspr1 ⊢ { +∞ } ⊆ { +∞ , -∞ }
16 15 12 sstri ⊢ { +∞ } ⊆ ℝ*
17 xpss12 ⊢ ( ( ( ℝ ∪ { -∞ } ) ⊆ ℝ* ∧ { +∞ } ⊆ ℝ* ) → ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ⊆ ( ℝ* × ℝ* ) )
18 14 16 17 mp2an ⊢ ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ⊆ ( ℝ* × ℝ* )
19 xpss12 ⊢ ( ( { -∞ } ⊆ ℝ* ∧ ℝ ⊆ ℝ* ) → ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* ) )
20 13 8 19 mp2an ⊢ ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* )
21 18 20 unssi ⊢ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ⊆ ( ℝ* × ℝ* )
22 7 21 unssi ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ) ⊆ ( ℝ* × ℝ* )
23 1 22 eqsstri ⊢ < ⊆ ( ℝ* × ℝ* )