| Step | Hyp | Ref
| Expression |
| 1 | | brun 5194 |
. . . . 5
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ↔ (𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵)) |
| 2 | | brxp 5734 |
. . . . . . 7
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ↔
(𝐴 ∈ (ℝ ∪
{-∞}) ∧ 𝐵 ∈
{+∞})) |
| 3 | | elsni 4643 |
. . . . . . . 8
⊢ (𝐵 ∈ {+∞} → 𝐵 = +∞) |
| 4 | | pnfnre 11302 |
. . . . . . . . . 10
⊢ +∞
∉ ℝ |
| 5 | 4 | neli 3048 |
. . . . . . . . 9
⊢ ¬
+∞ ∈ ℝ |
| 6 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
| 7 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝐵 = +∞ → (𝐵 ∈ ℝ ↔ +∞
∈ ℝ)) |
| 8 | 6, 7 | imbitrid 244 |
. . . . . . . . 9
⊢ (𝐵 = +∞ → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → +∞
∈ ℝ)) |
| 9 | 5, 8 | mtoi 199 |
. . . . . . . 8
⊢ (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
| 10 | 3, 9 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ {+∞} → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
| 11 | 2, 10 | simplbiim 504 |
. . . . . 6
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
¬ (𝐴 ∈ ℝ
∧ 𝐵 ∈
ℝ)) |
| 12 | | brxp 5734 |
. . . . . . 7
⊢ (𝐴({-∞} ×
ℝ)𝐵 ↔ (𝐴 ∈ {-∞} ∧ 𝐵 ∈
ℝ)) |
| 13 | | elsni 4643 |
. . . . . . . . 9
⊢ (𝐴 ∈ {-∞} → 𝐴 = -∞) |
| 14 | | mnfnre 11304 |
. . . . . . . . . . 11
⊢ -∞
∉ ℝ |
| 15 | 14 | neli 3048 |
. . . . . . . . . 10
⊢ ¬
-∞ ∈ ℝ |
| 16 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
| 17 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ↔ -∞
∈ ℝ)) |
| 18 | 16, 17 | imbitrid 244 |
. . . . . . . . . 10
⊢ (𝐴 = -∞ → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -∞
∈ ℝ)) |
| 19 | 15, 18 | mtoi 199 |
. . . . . . . . 9
⊢ (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
| 20 | 13, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ {-∞} → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
| 21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ {-∞} ∧ 𝐵 ∈ ℝ) → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
| 22 | 12, 21 | sylbi 217 |
. . . . . 6
⊢ (𝐴({-∞} ×
ℝ)𝐵 → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
| 23 | 11, 22 | jaoi 858 |
. . . . 5
⊢ ((𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ∨
𝐴({-∞} ×
ℝ)𝐵) → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
| 24 | 1, 23 | sylbi 217 |
. . . 4
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
| 25 | 24 | con2i 139 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵) |
| 26 | | df-ltxr 11300 |
. . . . . . 7
⊢ < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |
| 27 | 26 | equncomi 4160 |
. . . . . 6
⊢ < =
((((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} ×
ℝ)) ∪ {〈𝑥,
𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}) |
| 28 | 27 | breqi 5149 |
. . . . 5
⊢ (𝐴 < 𝐵 ↔ 𝐴((((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)) ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)})𝐵) |
| 29 | | brun 5194 |
. . . . 5
⊢ (𝐴((((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ)) ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)})𝐵 ↔ (𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 30 | | df-or 849 |
. . . . 5
⊢ ((𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵) ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 31 | 28, 29, 30 | 3bitri 297 |
. . . 4
⊢ (𝐴 < 𝐵 ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 32 | | biimt 360 |
. . . 4
⊢ (¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵 → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵))) |
| 33 | 31, 32 | bitr4id 290 |
. . 3
⊢ (¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵 → (𝐴 < 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 34 | 25, 33 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 35 | | breq12 5148 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵)) |
| 36 | | df-3an 1089 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) ↔ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)) |
| 37 | 36 | opabbii 5210 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)} |
| 38 | 35, 37 | brab2a 5779 |
. . 3
⊢ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵)) |
| 39 | 38 | baibr 536 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
| 40 | 34, 39 | bitr4d 282 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) |