Definition df-meas 32064

Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto (0[,]+∞). (Contributed by Thierry Arnoux, 10-Sep-2016.)

Assertion

Ref	Expression
df-meas	⊢ measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

Distinct variable group:   𝑥,𝑚,𝑦,𝑠

Detailed syntax breakdown of Definition df-meas

Step	Hyp	Ref	Expression
1		cmeas 32063	. 2 class measures
2		vs	. . 3 setvar 𝑠
3		csiga 31976	. . . . 5 class sigAlgebra
4	3	crn 5581	. . . 4 class ran sigAlgebra
5	4	cuni 4836	. . 3 class ∪ ran sigAlgebra
6	2	cv 1538	. . . . . 6 class 𝑠
7		cc0 10802	. . . . . . 7 class 0
8		cpnf 10937	. . . . . . 7 class +∞
9		cicc 13011	. . . . . . 7 class [,]
10	7, 8, 9	co 7255	. . . . . 6 class (0[,]+∞)
11		vm	. . . . . . 7 setvar 𝑚
12	11	cv 1538	. . . . . 6 class 𝑚
13	6, 10, 12	wf 6414	. . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14		c0 4253	. . . . . . 7 class ∅
15	14, 12	cfv 6418	. . . . . 6 class (𝑚‘∅)
16	15, 7	wceq 1539	. . . . 5 wff (𝑚‘∅) = 0
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1538	. . . . . . . . 9 class 𝑥
19		com 7687	. . . . . . . . 9 class ω
20		cdom 8689	. . . . . . . . 9 class ≼
21	18, 19, 20	wbr 5070	. . . . . . . 8 wff 𝑥 ≼ ω
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1538	. . . . . . . . 9 class 𝑦
24	22, 18, 23	wdisj 5035	. . . . . . . 8 wff Disj 𝑦 ∈ 𝑥 𝑦
25	21, 24	wa 395	. . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)
26	18	cuni 4836	. . . . . . . . 9 class ∪ 𝑥
27	26, 12	cfv 6418	. . . . . . . 8 class (𝑚‘∪ 𝑥)
28	23, 12	cfv 6418	. . . . . . . . 9 class (𝑚‘𝑦)
29	18, 28, 22	cesum 31895	. . . . . . . 8 class Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
30	27, 29	wceq 1539	. . . . . . 7 wff (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
31	25, 30	wi 4	. . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
32	6	cpw 4530	. . . . . 6 class 𝒫 𝑠
33	31, 17, 32	wral 3063	. . . . 5 wff ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
34	13, 16, 33	w3a 1085	. . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))
35	34, 11	cab 2715	. . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}
36	2, 5, 35	cmpt 5153	. 2 class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
37	1, 36	wceq 1539	1 wff measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

This definition is referenced by:  measbase  32065  measval  32066  ismeas  32067  isrnmeas  32068  measbasedom  32070