Step | Hyp | Ref
| Expression |
1 | | df-ltxr 7946 |
. . . . 5
⊢ < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |
2 | 1 | breqi 3993 |
. . . 4
⊢ (𝐴 < 𝐵 ↔ 𝐴({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))𝐵) |
3 | | brun 4038 |
. . . 4
⊢ (𝐴({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))𝐵 ↔ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵)) |
4 | 2, 3 | bitri 183 |
. . 3
⊢ (𝐴 < 𝐵 ↔ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵)) |
5 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ℝ ↔ 𝐴 ∈ ℝ)) |
6 | | breq1 3990 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝑦)) |
7 | 5, 6 | 3anbi13d 1309 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) ↔ (𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝐴 <ℝ 𝑦))) |
8 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 ∈ ℝ ↔ 𝐵 ∈ ℝ)) |
9 | | breq2 3991 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵)) |
10 | 8, 9 | 3anbi23d 1310 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝐴 <ℝ 𝑦) ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵))) |
11 | | eqid 2170 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} |
12 | 7, 10, 11 | brabg 4252 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵))) |
13 | | simp3 994 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵) → 𝐴 <ℝ 𝐵) |
14 | 12, 13 | syl6bi 162 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 → 𝐴 <ℝ 𝐵)) |
15 | | brun 4038 |
. . . . 5
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ↔ (𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵)) |
16 | | brxp 4640 |
. . . . . . . . . . 11
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ↔
(𝐴 ∈ (ℝ ∪
{-∞}) ∧ 𝐵 ∈
{+∞})) |
17 | 16 | simprbi 273 |
. . . . . . . . . 10
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
𝐵 ∈
{+∞}) |
18 | | elsni 3599 |
. . . . . . . . . 10
⊢ (𝐵 ∈ {+∞} → 𝐵 = +∞) |
19 | 17, 18 | syl 14 |
. . . . . . . . 9
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
𝐵 =
+∞) |
20 | 19 | a1i 9 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
𝐵 =
+∞)) |
21 | | renepnf 7954 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞) |
22 | 21 | neneqd 2361 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → ¬
𝐵 =
+∞) |
23 | | pm2.24 616 |
. . . . . . . 8
⊢ (𝐵 = +∞ → (¬ 𝐵 = +∞ → 𝐴 <ℝ 𝐵)) |
24 | 20, 22, 23 | syl6ci 1438 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
𝐴 <ℝ
𝐵)) |
25 | 24 | adantl 275 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 →
𝐴 <ℝ
𝐵)) |
26 | | brxp 4640 |
. . . . . . . . . . 11
⊢ (𝐴({-∞} ×
ℝ)𝐵 ↔ (𝐴 ∈ {-∞} ∧ 𝐵 ∈
ℝ)) |
27 | 26 | simplbi 272 |
. . . . . . . . . 10
⊢ (𝐴({-∞} ×
ℝ)𝐵 → 𝐴 ∈
{-∞}) |
28 | | elsni 3599 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {-∞} → 𝐴 = -∞) |
29 | 27, 28 | syl 14 |
. . . . . . . . 9
⊢ (𝐴({-∞} ×
ℝ)𝐵 → 𝐴 = -∞) |
30 | 29 | a1i 9 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴({-∞} ×
ℝ)𝐵 → 𝐴 = -∞)) |
31 | | renemnf 7955 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
32 | 31 | neneqd 2361 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ¬
𝐴 =
-∞) |
33 | | pm2.24 616 |
. . . . . . . 8
⊢ (𝐴 = -∞ → (¬ 𝐴 = -∞ → 𝐴 <ℝ 𝐵)) |
34 | 30, 32, 33 | syl6ci 1438 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴({-∞} ×
ℝ)𝐵 → 𝐴 <ℝ 𝐵)) |
35 | 34 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴({-∞} ×
ℝ)𝐵 → 𝐴 <ℝ 𝐵)) |
36 | 25, 35 | jaod 712 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ∨
𝐴({-∞} ×
ℝ)𝐵) → 𝐴 <ℝ 𝐵)) |
37 | 15, 36 | syl5bi 151 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 → 𝐴 <ℝ 𝐵)) |
38 | 14, 37 | jaod 712 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵) → 𝐴 <ℝ 𝐵)) |
39 | 4, 38 | syl5bi 151 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 <ℝ 𝐵)) |
40 | 12 | 3adant3 1012 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵) → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵))) |
41 | 40 | ibir 176 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵) → 𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵) |
42 | 41 | orcd 728 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵) → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵)) |
43 | 42, 4 | sylibr 133 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 <ℝ 𝐵) → 𝐴 < 𝐵) |
44 | 43 | 3expia 1200 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 → 𝐴 < 𝐵)) |
45 | 39, 44 | impbid 128 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) |