Detailed syntax breakdown of Definition df-xadd
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cxad 12506 |
. 2
class
+𝑒 |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | vy |
. . 3
setvar 𝑦 |
| 4 | | cxr 10674 |
. . 3
class
ℝ* |
| 5 | 2 | cv 1536 |
. . . . 5
class 𝑥 |
| 6 | | cpnf 10672 |
. . . . 5
class
+∞ |
| 7 | 5, 6 | wceq 1537 |
. . . 4
wff 𝑥 = +∞ |
| 8 | 3 | cv 1536 |
. . . . . 6
class 𝑦 |
| 9 | | cmnf 10673 |
. . . . . 6
class
-∞ |
| 10 | 8, 9 | wceq 1537 |
. . . . 5
wff 𝑦 = -∞ |
| 11 | | cc0 10537 |
. . . . 5
class
0 |
| 12 | 10, 11, 6 | cif 4467 |
. . . 4
class if(𝑦 = -∞, 0,
+∞) |
| 13 | 5, 9 | wceq 1537 |
. . . . 5
wff 𝑥 = -∞ |
| 14 | 8, 6 | wceq 1537 |
. . . . . 6
wff 𝑦 = +∞ |
| 15 | 14, 11, 9 | cif 4467 |
. . . . 5
class if(𝑦 = +∞, 0,
-∞) |
| 16 | | caddc 10540 |
. . . . . . . 8
class
+ |
| 17 | 5, 8, 16 | co 7156 |
. . . . . . 7
class (𝑥 + 𝑦) |
| 18 | 10, 9, 17 | cif 4467 |
. . . . . 6
class if(𝑦 = -∞, -∞, (𝑥 + 𝑦)) |
| 19 | 14, 6, 18 | cif 4467 |
. . . . 5
class if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))) |
| 20 | 13, 15, 19 | cif 4467 |
. . . 4
class if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))) |
| 21 | 7, 12, 20 | cif 4467 |
. . 3
class if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞),
if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦))))) |
| 22 | 2, 3, 4, 4, 21 | cmpo 7158 |
. 2
class (𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))))) |
| 23 | 1, 22 | wceq 1537 |
1
wff
+𝑒 = (𝑥
∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞),
if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞),
if(𝑦 = +∞, +∞,
if(𝑦 = -∞, -∞,
(𝑥 + 𝑦)))))) |
