Detailed syntax breakdown of Definition df-itg1
| Step | Hyp | Ref
| Expression |
| 1 | | citg1 25650 |
. 2
class
∫1 |
| 2 | | vf |
. . 3
setvar 𝑓 |
| 3 | | cr 11154 |
. . . . . 6
class
ℝ |
| 4 | | vg |
. . . . . . 7
setvar 𝑔 |
| 5 | 4 | cv 1539 |
. . . . . 6
class 𝑔 |
| 6 | 3, 3, 5 | wf 6557 |
. . . . 5
wff 𝑔:ℝ⟶ℝ |
| 7 | 5 | crn 5686 |
. . . . . 6
class ran 𝑔 |
| 8 | | cfn 8985 |
. . . . . 6
class
Fin |
| 9 | 7, 8 | wcel 2108 |
. . . . 5
wff ran 𝑔 ∈ Fin |
| 10 | 5 | ccnv 5684 |
. . . . . . . 8
class ◡𝑔 |
| 11 | | cc0 11155 |
. . . . . . . . . 10
class
0 |
| 12 | 11 | csn 4626 |
. . . . . . . . 9
class
{0} |
| 13 | 3, 12 | cdif 3948 |
. . . . . . . 8
class (ℝ
∖ {0}) |
| 14 | 10, 13 | cima 5688 |
. . . . . . 7
class (◡𝑔 “ (ℝ ∖
{0})) |
| 15 | | cvol 25498 |
. . . . . . 7
class
vol |
| 16 | 14, 15 | cfv 6561 |
. . . . . 6
class
(vol‘(◡𝑔 “ (ℝ ∖
{0}))) |
| 17 | 16, 3 | wcel 2108 |
. . . . 5
wff
(vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈
ℝ |
| 18 | 6, 9, 17 | w3a 1087 |
. . . 4
wff (𝑔:ℝ⟶ℝ ∧
ran 𝑔 ∈ Fin ∧
(vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈
ℝ) |
| 19 | | cmbf 25649 |
. . . 4
class
MblFn |
| 20 | 18, 4, 19 | crab 3436 |
. . 3
class {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧
ran 𝑔 ∈ Fin ∧
(vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈
ℝ)} |
| 21 | 2 | cv 1539 |
. . . . . 6
class 𝑓 |
| 22 | 21 | crn 5686 |
. . . . 5
class ran 𝑓 |
| 23 | 22, 12 | cdif 3948 |
. . . 4
class (ran
𝑓 ∖
{0}) |
| 24 | | vx |
. . . . . 6
setvar 𝑥 |
| 25 | 24 | cv 1539 |
. . . . 5
class 𝑥 |
| 26 | 21 | ccnv 5684 |
. . . . . . 7
class ◡𝑓 |
| 27 | 25 | csn 4626 |
. . . . . . 7
class {𝑥} |
| 28 | 26, 27 | cima 5688 |
. . . . . 6
class (◡𝑓 “ {𝑥}) |
| 29 | 28, 15 | cfv 6561 |
. . . . 5
class
(vol‘(◡𝑓 “ {𝑥})) |
| 30 | | cmul 11160 |
. . . . 5
class
· |
| 31 | 25, 29, 30 | co 7431 |
. . . 4
class (𝑥 · (vol‘(◡𝑓 “ {𝑥}))) |
| 32 | 23, 31, 24 | csu 15722 |
. . 3
class
Σ𝑥 ∈ (ran
𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))) |
| 33 | 2, 20, 32 | cmpt 5225 |
. 2
class (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧
(vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈
ℝ)} ↦ Σ𝑥
∈ (ran 𝑓 ∖
{0})(𝑥 ·
(vol‘(◡𝑓 “ {𝑥})))) |
| 34 | 1, 33 | wceq 1540 |
1
wff
∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧
(vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈
ℝ)} ↦ Σ𝑥
∈ (ran 𝑓 ∖
{0})(𝑥 ·
(vol‘(◡𝑓 “ {𝑥})))) |