Step | Hyp | Ref
| Expression |
1 | | breq12 3760 |
. . . . 5
⊢
((x = A ∧ y = B) →
(x <ℝ y ↔ A
<ℝ B)) |
2 | | df-3an 886 |
. . . . . 6
⊢
((x ∈ ℝ ∧
y ∈
ℝ ∧ x <ℝ y) ↔ ((x
∈ ℝ ∧
y ∈
ℝ) ∧ x <ℝ y)) |
3 | 2 | opabbii 3815 |
. . . . 5
⊢
{〈x, y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)} = {〈x,
y〉 ∣ ((x ∈ ℝ ∧ y ∈ ℝ) ∧
x <ℝ y)} |
4 | 1, 3 | brab2ga 4358 |
. . . 4
⊢ (A{〈x,
y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)}B ↔
((A ∈
ℝ ∧ B ∈ ℝ) ∧ A
<ℝ B)) |
5 | 4 | a1i 9 |
. . 3
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → (A{〈x,
y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)}B ↔
((A ∈
ℝ ∧ B ∈ ℝ) ∧ A
<ℝ B))) |
6 | | brun 3801 |
. . . 4
⊢ (A(((ℝ ∪ {-∞}) × {+∞})
∪ ({-∞} × ℝ))B ↔
(A((ℝ ∪ {-∞}) ×
{+∞})B
∨ A({-∞} ×
ℝ)B)) |
7 | | brxp 4318 |
. . . . . . 7
⊢ (A((ℝ ∪ {-∞}) ×
{+∞})B ↔ (A ∈ (ℝ ∪
{-∞}) ∧ B ∈
{+∞})) |
8 | | elun 3078 |
. . . . . . . . . . 11
⊢ (A ∈ (ℝ ∪
{-∞}) ↔ (A ∈ ℝ ∨
A ∈
{-∞})) |
9 | | orcom 646 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∨
A ∈
{-∞}) ↔ (A ∈ {-∞} ∨
A ∈
ℝ)) |
10 | 8, 9 | bitri 173 |
. . . . . . . . . 10
⊢ (A ∈ (ℝ ∪
{-∞}) ↔ (A ∈ {-∞} ∨
A ∈
ℝ)) |
11 | | elsncg 3389 |
. . . . . . . . . . 11
⊢ (A ∈
ℝ* → (A ∈ {-∞} ↔ A = -∞)) |
12 | 11 | orbi1d 704 |
. . . . . . . . . 10
⊢ (A ∈
ℝ* → ((A ∈ {-∞} ∨
A ∈
ℝ) ↔ (A = -∞ ∨ A ∈ ℝ))) |
13 | 10, 12 | syl5bb 181 |
. . . . . . . . 9
⊢ (A ∈
ℝ* → (A ∈ (ℝ ∪ {-∞}) ↔ (A = -∞ ∨
A ∈
ℝ))) |
14 | | elsncg 3389 |
. . . . . . . . 9
⊢ (B ∈
ℝ* → (B ∈ {+∞} ↔ B = +∞)) |
15 | 13, 14 | bi2anan9 538 |
. . . . . . . 8
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ (ℝ ∪
{-∞}) ∧ B ∈ {+∞})
↔ ((A = -∞ ∨ A ∈ ℝ) ∧
B = +∞))) |
16 | | andir 731 |
. . . . . . . 8
⊢
(((A = -∞ ∨ A ∈ ℝ) ∧
B = +∞) ↔ ((A = -∞ ∧
B = +∞)
∨ (A ∈ ℝ ∧
B = +∞))) |
17 | 15, 16 | syl6bb 185 |
. . . . . . 7
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ (ℝ ∪
{-∞}) ∧ B ∈ {+∞})
↔ ((A = -∞ ∧ B = +∞)
∨ (A ∈ ℝ ∧
B = +∞)))) |
18 | 7, 17 | syl5bb 181 |
. . . . . 6
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → (A((ℝ ∪ {-∞}) ×
{+∞})B ↔ ((A = -∞ ∧
B = +∞)
∨ (A ∈ ℝ ∧
B = +∞)))) |
19 | | brxp 4318 |
. . . . . . 7
⊢ (A({-∞} × ℝ)B ↔ (A
∈ {-∞} ∧ B ∈ ℝ)) |
20 | 11 | anbi1d 438 |
. . . . . . . 8
⊢ (A ∈
ℝ* → ((A ∈ {-∞} ∧
B ∈
ℝ) ↔ (A = -∞ ∧ B ∈ ℝ))) |
21 | 20 | adantr 261 |
. . . . . . 7
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ {-∞}
∧ B ∈ ℝ) ↔ (A = -∞ ∧
B ∈
ℝ))) |
22 | 19, 21 | syl5bb 181 |
. . . . . 6
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → (A({-∞} × ℝ)B ↔ (A =
-∞ ∧ B ∈
ℝ))) |
23 | 18, 22 | orbi12d 706 |
. . . . 5
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A((ℝ ∪ {-∞}) ×
{+∞})B
∨ A({-∞} ×
ℝ)B) ↔ (((A = -∞ ∧
B = +∞)
∨ (A ∈ ℝ ∧
B = +∞))
∨ (A = -∞ ∧ B ∈ ℝ)))) |
24 | | orass 683 |
. . . . 5
⊢
((((A = -∞ ∧ B = +∞)
∨ (A ∈ ℝ ∧
B = +∞))
∨ (A = -∞ ∧ B ∈ ℝ)) ↔ ((A = -∞ ∧
B = +∞)
∨ ((A ∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ)))) |
25 | 23, 24 | syl6bb 185 |
. . . 4
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A((ℝ ∪ {-∞}) ×
{+∞})B
∨ A({-∞} ×
ℝ)B) ↔ ((A = -∞ ∧
B = +∞)
∨ ((A ∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ))))) |
26 | 6, 25 | syl5bb 181 |
. . 3
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(((ℝ ∪ {-∞}) × {+∞})
∪ ({-∞} × ℝ))B ↔
((A = -∞ ∧ B = +∞)
∨ ((A
∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ))))) |
27 | 5, 26 | orbi12d 706 |
. 2
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A{〈x,
y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)}B ∨ A(((ℝ
∪ {-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))B) ↔ (((A ∈ ℝ ∧ B ∈ ℝ) ∧
A <ℝ B) ∨ ((A = -∞ ∧
B = +∞)
∨ ((A ∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ)))))) |
28 | | df-ltxr 6862 |
. . . 4
⊢ < =
({〈x, y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ))) |
29 | 28 | breqi 3761 |
. . 3
⊢ (A < B ↔
A({〈x, y〉
∣ (x ∈ ℝ ∧
y ∈
ℝ ∧ x <ℝ y)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))B) |
30 | | brun 3801 |
. . 3
⊢ (A({〈x,
y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)} ∪ (((ℝ ∪ {-∞}) ×
{+∞}) ∪ ({-∞} × ℝ)))B ↔ (A{〈x,
y〉 ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧
x <ℝ y)}B ∨ A(((ℝ
∪ {-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))B)) |
31 | 29, 30 | bitri 173 |
. 2
⊢ (A < B ↔
(A{〈x, y〉
∣ (x ∈ ℝ ∧
y ∈
ℝ ∧ x <ℝ y)}B ∨ A(((ℝ
∪ {-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))B)) |
32 | | orass 683 |
. 2
⊢
(((((A ∈ ℝ ∧
B ∈
ℝ) ∧ A <ℝ B) ∨ (A = -∞ ∧
B = +∞))
∨ ((A ∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ))) ↔ (((A ∈ ℝ ∧ B ∈ ℝ) ∧
A <ℝ B) ∨ ((A = -∞ ∧
B = +∞)
∨ ((A ∈ ℝ ∧
B = +∞)
∨ (A = -∞ ∧ B ∈ ℝ))))) |
33 | 27, 31, 32 | 3bitr4g 212 |
1
⊢
((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔
((((A ∈
ℝ ∧ B ∈ ℝ) ∧ A
<ℝ B) ∨ (A = -∞
∧ B =
+∞)) ∨ ((A ∈ ℝ ∧ B = +∞)
∨ (A =
-∞ ∧ B ∈
ℝ))))) |