| Step | Hyp | Ref
| Expression |
| 1 | | df-ltxr 11300 |
. 2
⊢ < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |
| 2 | | df-3an 1089 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) ↔ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)) |
| 3 | 2 | opabbii 5210 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)} |
| 4 | | opabssxp 5778 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)} ⊆ (ℝ ×
ℝ) |
| 5 | 3, 4 | eqsstri 4030 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ⊆ (ℝ ×
ℝ) |
| 6 | | rexpssxrxp 11306 |
. . . 4
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 7 | 5, 6 | sstri 3993 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ⊆ (ℝ*
× ℝ*) |
| 8 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 9 | | snsspr2 4815 |
. . . . . . 7
⊢
{-∞} ⊆ {+∞, -∞} |
| 10 | | ssun2 4179 |
. . . . . . . 8
⊢
{+∞, -∞} ⊆ (ℝ ∪ {+∞,
-∞}) |
| 11 | | df-xr 11299 |
. . . . . . . 8
⊢
ℝ* = (ℝ ∪ {+∞,
-∞}) |
| 12 | 10, 11 | sseqtrri 4033 |
. . . . . . 7
⊢
{+∞, -∞} ⊆ ℝ* |
| 13 | 9, 12 | sstri 3993 |
. . . . . 6
⊢
{-∞} ⊆ ℝ* |
| 14 | 8, 13 | unssi 4191 |
. . . . 5
⊢ (ℝ
∪ {-∞}) ⊆ ℝ* |
| 15 | | snsspr1 4814 |
. . . . . 6
⊢
{+∞} ⊆ {+∞, -∞} |
| 16 | 15, 12 | sstri 3993 |
. . . . 5
⊢
{+∞} ⊆ ℝ* |
| 17 | | xpss12 5700 |
. . . . 5
⊢
(((ℝ ∪ {-∞}) ⊆ ℝ* ∧
{+∞} ⊆ ℝ*) → ((ℝ ∪ {-∞})
× {+∞}) ⊆ (ℝ* ×
ℝ*)) |
| 18 | 14, 16, 17 | mp2an 692 |
. . . 4
⊢ ((ℝ
∪ {-∞}) × {+∞}) ⊆ (ℝ* ×
ℝ*) |
| 19 | | xpss12 5700 |
. . . . 5
⊢
(({-∞} ⊆ ℝ* ∧ ℝ ⊆
ℝ*) → ({-∞} × ℝ) ⊆
(ℝ* × ℝ*)) |
| 20 | 13, 8, 19 | mp2an 692 |
. . . 4
⊢
({-∞} × ℝ) ⊆ (ℝ* ×
ℝ*) |
| 21 | 18, 20 | unssi 4191 |
. . 3
⊢
(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞}
× ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 22 | 7, 21 | unssi 4191 |
. 2
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))) ⊆
(ℝ* × ℝ*) |
| 23 | 1, 22 | eqsstri 4030 |
1
⊢ <
⊆ (ℝ* × ℝ*) |