# 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 ${⊢}<\subseteq {ℝ}^{*}×{ℝ}^{*}$

### Proof

Step Hyp Ref Expression
1 df-ltxr ${⊢}<=\left\{⟨{x},{y}⟩|\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)\right\}\cup \left(\left(\left(ℝ\cup \left\{\mathrm{-\infty }\right\}\right)×\left\{\mathrm{+\infty }\right\}\right)\cup \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\right)$
2 df-3an ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)↔\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {x}{<}_{ℝ}{y}\right)$
3 2 opabbii ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)\right\}=\left\{⟨{x},{y}⟩|\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {x}{<}_{ℝ}{y}\right)\right\}$
4 opabssxp ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {x}{<}_{ℝ}{y}\right)\right\}\subseteq {ℝ}^{2}$
5 3 4 eqsstri ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)\right\}\subseteq {ℝ}^{2}$
6 rexpssxrxp ${⊢}{ℝ}^{2}\subseteq {ℝ}^{*}×{ℝ}^{*}$
7 5 6 sstri ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)\right\}\subseteq {ℝ}^{*}×{ℝ}^{*}$
8 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
9 snsspr2 ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$
10 ssun2 ${⊢}\left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\subseteq ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$
11 df-xr ${⊢}{ℝ}^{*}=ℝ\cup \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$
12 10 11 sseqtrri ${⊢}\left\{\mathrm{+\infty },\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
13 9 12 sstri ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
14 8 13 unssi ${⊢}ℝ\cup \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
15 snsspr1 ${⊢}\left\{\mathrm{+\infty }\right\}\subseteq \left\{\mathrm{+\infty },\mathrm{-\infty }\right\}$
16 15 12 sstri ${⊢}\left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}$
17 xpss12 ${⊢}\left(ℝ\cup \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\wedge \left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}\right)\to \left(ℝ\cup \left\{\mathrm{-\infty }\right\}\right)×\left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}×{ℝ}^{*}$
18 14 16 17 mp2an ${⊢}\left(ℝ\cup \left\{\mathrm{-\infty }\right\}\right)×\left\{\mathrm{+\infty }\right\}\subseteq {ℝ}^{*}×{ℝ}^{*}$
19 xpss12 ${⊢}\left(\left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\wedge ℝ\subseteq {ℝ}^{*}\right)\to \left\{\mathrm{-\infty }\right\}×ℝ\subseteq {ℝ}^{*}×{ℝ}^{*}$
20 13 8 19 mp2an ${⊢}\left\{\mathrm{-\infty }\right\}×ℝ\subseteq {ℝ}^{*}×{ℝ}^{*}$
21 18 20 unssi ${⊢}\left(\left(ℝ\cup \left\{\mathrm{-\infty }\right\}\right)×\left\{\mathrm{+\infty }\right\}\right)\cup \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\subseteq {ℝ}^{*}×{ℝ}^{*}$
22 7 21 unssi ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in ℝ\wedge {y}\in ℝ\wedge {x}{<}_{ℝ}{y}\right)\right\}\cup \left(\left(\left(ℝ\cup \left\{\mathrm{-\infty }\right\}\right)×\left\{\mathrm{+\infty }\right\}\right)\cup \left(\left\{\mathrm{-\infty }\right\}×ℝ\right)\right)\subseteq {ℝ}^{*}×{ℝ}^{*}$
23 1 22 eqsstri ${⊢}<\subseteq {ℝ}^{*}×{ℝ}^{*}$