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	⊢ < ⊆ ( ℝ* × ℝ* )