Detailed syntax breakdown of Definition df-meas
Step | Hyp | Ref
| Expression |
1 | | cmeas 32159 |
. 2
class
measures |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | csiga 32072 |
. . . . 5
class
sigAlgebra |
4 | 3 | crn 5591 |
. . . 4
class ran
sigAlgebra |
5 | 4 | cuni 4845 |
. . 3
class ∪ ran sigAlgebra |
6 | 2 | cv 1541 |
. . . . . 6
class 𝑠 |
7 | | cc0 10872 |
. . . . . . 7
class
0 |
8 | | cpnf 11007 |
. . . . . . 7
class
+∞ |
9 | | cicc 13081 |
. . . . . . 7
class
[,] |
10 | 7, 8, 9 | co 7271 |
. . . . . 6
class
(0[,]+∞) |
11 | | vm |
. . . . . . 7
setvar 𝑚 |
12 | 11 | cv 1541 |
. . . . . 6
class 𝑚 |
13 | 6, 10, 12 | wf 6428 |
. . . . 5
wff 𝑚:𝑠⟶(0[,]+∞) |
14 | | c0 4262 |
. . . . . . 7
class
∅ |
15 | 14, 12 | cfv 6432 |
. . . . . 6
class (𝑚‘∅) |
16 | 15, 7 | wceq 1542 |
. . . . 5
wff (𝑚‘∅) =
0 |
17 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
18 | 17 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
19 | | com 7706 |
. . . . . . . . 9
class
ω |
20 | | cdom 8714 |
. . . . . . . . 9
class
≼ |
21 | 18, 19, 20 | wbr 5079 |
. . . . . . . 8
wff 𝑥 ≼
ω |
22 | | vy |
. . . . . . . . 9
setvar 𝑦 |
23 | 22 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
24 | 22, 18, 23 | wdisj 5044 |
. . . . . . . 8
wff Disj
𝑦 ∈ 𝑥 𝑦 |
25 | 21, 24 | wa 396 |
. . . . . . 7
wff (𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) |
26 | 18 | cuni 4845 |
. . . . . . . . 9
class ∪ 𝑥 |
27 | 26, 12 | cfv 6432 |
. . . . . . . 8
class (𝑚‘∪ 𝑥) |
28 | 23, 12 | cfv 6432 |
. . . . . . . . 9
class (𝑚‘𝑦) |
29 | 18, 28, 22 | cesum 31991 |
. . . . . . . 8
class
Σ*𝑦
∈ 𝑥(𝑚‘𝑦) |
30 | 27, 29 | wceq 1542 |
. . . . . . 7
wff (𝑚‘∪ 𝑥) =
Σ*𝑦 ∈
𝑥(𝑚‘𝑦) |
31 | 25, 30 | wi 4 |
. . . . . 6
wff ((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) |
32 | 6 | cpw 4539 |
. . . . . 6
class 𝒫
𝑠 |
33 | 31, 17, 32 | wral 3066 |
. . . . 5
wff
∀𝑥 ∈
𝒫 𝑠((𝑥 ≼ ω ∧
Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)) |
34 | 13, 16, 33 | w3a 1086 |
. . . 4
wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))) |
35 | 34, 11 | cab 2717 |
. . 3
class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))} |
36 | 2, 5, 35 | cmpt 5162 |
. 2
class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) |
37 | 1, 36 | wceq 1542 |
1
wff measures =
(𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧
∀𝑥 ∈ 𝒫
𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}) |