| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq12 5148 | . . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵)) | 
| 2 |  | df-3an 1089 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) ↔ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)) | 
| 3 | 2 | opabbii 5210 | . . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 <ℝ 𝑦)} | 
| 4 | 1, 3 | brab2a 5779 | . . . 4
⊢ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵)) | 
| 5 | 4 | a1i 11 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ↔ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵))) | 
| 6 |  | brun 5194 | . . . 4
⊢ (𝐴(((ℝ ∪ {-∞})
× {+∞}) ∪ ({-∞} × ℝ))𝐵 ↔ (𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵)) | 
| 7 |  | brxp 5734 | . . . . . . 7
⊢ (𝐴((ℝ ∪ {-∞})
× {+∞})𝐵 ↔
(𝐴 ∈ (ℝ ∪
{-∞}) ∧ 𝐵 ∈
{+∞})) | 
| 8 |  | elun 4153 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (ℝ ∪
{-∞}) ↔ (𝐴
∈ ℝ ∨ 𝐴
∈ {-∞})) | 
| 9 |  | orcom 871 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {-∞}) ↔
(𝐴 ∈ {-∞} ∨
𝐴 ∈
ℝ)) | 
| 10 | 8, 9 | bitri 275 | . . . . . . . . . 10
⊢ (𝐴 ∈ (ℝ ∪
{-∞}) ↔ (𝐴
∈ {-∞} ∨ 𝐴
∈ ℝ)) | 
| 11 |  | elsng 4640 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ (𝐴 ∈ {-∞}
↔ 𝐴 =
-∞)) | 
| 12 | 11 | orbi1d 917 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℝ*
→ ((𝐴 ∈
{-∞} ∨ 𝐴 ∈
ℝ) ↔ (𝐴 =
-∞ ∨ 𝐴 ∈
ℝ))) | 
| 13 | 10, 12 | bitrid 283 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
→ (𝐴 ∈ (ℝ
∪ {-∞}) ↔ (𝐴
= -∞ ∨ 𝐴 ∈
ℝ))) | 
| 14 |  | elsng 4640 | . . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ∈ {+∞}
↔ 𝐵 =
+∞)) | 
| 15 | 13, 14 | bi2anan9 638 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴 ∈ (ℝ ∪ {-∞}) ∧
𝐵 ∈ {+∞}) ↔
((𝐴 = -∞ ∨ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞))) | 
| 16 |  | andir 1011 | . . . . . . . 8
⊢ (((𝐴 = -∞ ∨ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) ↔ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ (𝐴 ∈ ℝ ∧ 𝐵 = +∞))) | 
| 17 | 15, 16 | bitrdi 287 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴 ∈ (ℝ ∪ {-∞}) ∧
𝐵 ∈ {+∞}) ↔
((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ (𝐴 ∈ ℝ ∧ 𝐵 = +∞)))) | 
| 18 | 7, 17 | bitrid 283 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ↔ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ (𝐴 ∈ ℝ ∧ 𝐵 = +∞)))) | 
| 19 |  | brxp 5734 | . . . . . . 7
⊢ (𝐴({-∞} ×
ℝ)𝐵 ↔ (𝐴 ∈ {-∞} ∧ 𝐵 ∈
ℝ)) | 
| 20 | 11 | anbi1d 631 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ*
→ ((𝐴 ∈
{-∞} ∧ 𝐵 ∈
ℝ) ↔ (𝐴 =
-∞ ∧ 𝐵 ∈
ℝ))) | 
| 21 | 20 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴 ∈ {-∞} ∧ 𝐵 ∈ ℝ) ↔ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))) | 
| 22 | 19, 21 | bitrid 283 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴({-∞} × ℝ)𝐵 ↔ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))) | 
| 23 | 18, 22 | orbi12d 919 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵) ↔ (((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ (𝐴 ∈ ℝ ∧ 𝐵 = +∞)) ∨ (𝐴 = -∞ ∧ 𝐵 ∈
ℝ)))) | 
| 24 |  | orass 922 | . . . . 5
⊢ ((((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ (𝐴 ∈ ℝ ∧ 𝐵 = +∞)) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)) ↔ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈
ℝ)))) | 
| 25 | 23, 24 | bitrdi 287 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴((ℝ ∪ {-∞}) ×
{+∞})𝐵 ∨ 𝐴({-∞} ×
ℝ)𝐵) ↔ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈
ℝ))))) | 
| 26 | 6, 25 | bitrid 283 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵 ↔ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) | 
| 27 | 5, 26 | orbi12d 919 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵) ↔ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)))))) | 
| 28 |  | df-ltxr 11300 | . . . 4
⊢  < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) | 
| 29 | 28 | breqi 5149 | . . 3
⊢ (𝐴 < 𝐵 ↔ 𝐴({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))𝐵) | 
| 30 |  | brun 5194 | . . 3
⊢ (𝐴({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))𝐵 ↔ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵)) | 
| 31 | 29, 30 | bitri 275 | . 2
⊢ (𝐴 < 𝐵 ↔ (𝐴{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)}𝐵 ∨ 𝐴(((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))𝐵)) | 
| 32 |  | orass 922 | . 2
⊢
(((((𝐴 ∈
ℝ ∧ 𝐵 ∈
ℝ) ∧ 𝐴
<ℝ 𝐵)
∨ (𝐴 = -∞ ∧
𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))) ↔
(((𝐴 ∈ ℝ ∧
𝐵 ∈ ℝ) ∧
𝐴 <ℝ
𝐵) ∨ ((𝐴 = -∞ ∧ 𝐵 = +∞) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) | 
| 33 | 27, 31, 32 | 3bitr4g 314 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 <ℝ 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ))))) |