Definition df-meas 29586

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 29585	. 2 class measures
2		vs	. . 3 setvar 𝑠
3		csiga 29497	. . . . 5 class sigAlgebra
4	3	crn 5039	. . . 4 class ran sigAlgebra
5	4	cuni 4372	. . 3 class ∪ ran sigAlgebra
6	2	cv 1474	. . . . . 6 class 𝑠
7		cc0 9815	. . . . . . 7 class 0
8		cpnf 9950	. . . . . . 7 class +∞
9		cicc 12049	. . . . . . 7 class [,]
10	7, 8, 9	co 6549	. . . . . 6 class (0[,]+∞)
11		vm	. . . . . . 7 setvar 𝑚
12	11	cv 1474	. . . . . 6 class 𝑚
13	6, 10, 12	wf 5800	. . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14		c0 3874	. . . . . . 7 class ∅
15	14, 12	cfv 5804	. . . . . 6 class (𝑚‘∅)
16	15, 7	wceq 1475	. . . . 5 wff (𝑚‘∅) = 0
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1474	. . . . . . . . 9 class 𝑥
19		com 6957	. . . . . . . . 9 class ω
20		cdom 7839	. . . . . . . . 9 class ≼
21	18, 19, 20	wbr 4583	. . . . . . . 8 wff 𝑥 ≼ ω
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1474	. . . . . . . . 9 class 𝑦
24	22, 18, 23	wdisj 4553	. . . . . . . 8 wff Disj 𝑦 ∈ 𝑥 𝑦
25	21, 24	wa 383	. . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)
26	18	cuni 4372	. . . . . . . . 9 class ∪ 𝑥
27	26, 12	cfv 5804	. . . . . . . 8 class (𝑚‘∪ 𝑥)
28	23, 12	cfv 5804	. . . . . . . . 9 class (𝑚‘𝑦)
29	18, 28, 22	cesum 29416	. . . . . . . 8 class Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
30	27, 29	wceq 1475	. . . . . . 7 wff (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
31	25, 30	wi 4	. . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
32	6	cpw 4108	. . . . . 6 class 𝒫 𝑠
33	31, 17, 32	wral 2896	. . . . 5 wff ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
34	13, 16, 33	w3a 1031	. . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))
35	34, 11	cab 2596	. . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}
36	2, 5, 35	cmpt 4643	. 2 class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
37	1, 36	wceq 1475	1 wff measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

This definition is referenced by:  measbase  29587  measval  29588  ismeas  29589  isrnmeas  29590  measbasedom  29592