Step | Hyp | Ref
| Expression |
1 | | brun 4703 |
. . . . 5
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ↔ (𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵)) |
2 | | brxp 5147 |
. . . . . . 7
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ↔
(𝐴 ∈ (ℝ ∪
{-∞}) ∧ 𝐵 ∈
{+∞})) |
3 | | elsni 4194 |
. . . . . . . . 9
⊢ (𝐵 ∈ {+∞} → 𝐵 = +∞) |
4 | | pnfnre 10081 |
. . . . . . . . . . 11
⊢ +∞
∉ ℝ |
5 | 4 | neli 2899 |
. . . . . . . . . 10
⊢ ¬
+∞ ∈ ℝ |
6 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
7 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝐵 = +∞ → (𝐵 ∈ ℝ ↔ +∞
∈ ℝ)) |
8 | 6, 7 | syl5ib 234 |
. . . . . . . . . 10
⊢ (𝐵 = +∞ → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → +∞
∈ ℝ)) |
9 | 5, 8 | mtoi 190 |
. . . . . . . . 9
⊢ (𝐵 = +∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
10 | 3, 9 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ {+∞} → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
11 | 10 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ (ℝ ∪
{-∞}) ∧ 𝐵 ∈
{+∞}) → ¬ (𝐴
∈ ℝ ∧ 𝐵
∈ ℝ)) |
12 | 2, 11 | sylbi 207 |
. . . . . 6
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
¬ (𝐴 ∈ ℝ
∧ 𝐵 ∈
ℝ)) |
13 | | brxp 5147 |
. . . . . . 7
⊢ (𝐴({-∞} ×
ℝ)𝐵 ↔ (𝐴 ∈ {-∞} ∧ 𝐵 ∈
ℝ)) |
14 | | elsni 4194 |
. . . . . . . . 9
⊢ (𝐴 ∈ {-∞} → 𝐴 = -∞) |
15 | | mnfnre 10082 |
. . . . . . . . . . 11
⊢ -∞
∉ ℝ |
16 | 15 | neli 2899 |
. . . . . . . . . 10
⊢ ¬
-∞ ∈ ℝ |
17 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
18 | | eleq1 2689 |
. . . . . . . . . . 11
⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ↔ -∞
∈ ℝ)) |
19 | 17, 18 | syl5ib 234 |
. . . . . . . . . 10
⊢ (𝐴 = -∞ → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -∞
∈ ℝ)) |
20 | 16, 19 | mtoi 190 |
. . . . . . . . 9
⊢ (𝐴 = -∞ → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ)) |
21 | 14, 20 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ {-∞} → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ {-∞} ∧ 𝐵 ∈ ℝ) → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
23 | 13, 22 | sylbi 207 |
. . . . . 6
⊢ (𝐴({-∞} ×
ℝ)𝐵 → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
24 | 12, 23 | jaoi 394 |
. . . . 5
⊢ ((𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ∨
𝐴({-∞} ×
ℝ)𝐵) → ¬
(𝐴 ∈ ℝ ∧
𝐵 ∈
ℝ)) |
25 | 1, 24 | sylbi 207 |
. . . 4
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 → ¬ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
26 | 25 | con2i 134 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵) |
27 | | biimt 350 |
. . . 4
⊢ (¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵 → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵))) |
28 | | df-ltxr 10079 |
. . . . . . 7
⊢ < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |
29 | 28 | equncomi 3759 |
. . . . . 6
⊢ < =
((((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} ×
ℝ)) ∪ {〈𝑥,
𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}) |
30 | 29 | breqi 4659 |
. . . . 5
⊢ (𝐴 < 𝐵 ↔ 𝐴((((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)) ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)})𝐵) |
31 | | brun 4703 |
. . . . 5
⊢ (𝐴((((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ)) ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)})𝐵 ↔ (𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
32 | | df-or 385 |
. . . . 5
⊢ ((𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵) ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
33 | 30, 31, 32 | 3bitri 286 |
. . . 4
⊢ (𝐴 < 𝐵 ↔ (¬ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
34 | 27, 33 | syl6rbbr 279 |
. . 3
⊢ (¬
𝐴(((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} × ℝ))𝐵 → (𝐴 < 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
35 | 26, 34 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
36 | | breq12 4658 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵)) |
37 | | df-3an 1039 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) ↔ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)) |
38 | 37 | opabbii 4717 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)} |
39 | 36, 38 | brab2a 5194 |
. . 3
⊢ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵)) |
40 | 39 | baibr 945 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵)) |
41 | 35, 40 | bitr4d 271 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) |