Definition df-meas 34876

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 34875	. 2 class measures
2		vs	. . 3 setvar 𝑠
3		csiga 34787	. . . . 5 class sigAlgebra
4	3	crn 5651	. . . 4 class ran sigAlgebra
5	4	cuni 4866	. . 3 class ∪ ran sigAlgebra
6	2	cv 1568	. . . . . 6 class 𝑠
7		cc0 11204	. . . . . . 7 class 0
8		cpnf 11344	. . . . . . 7 class +∞
9		cicc 13483	. . . . . . 7 class [,]
10	7, 8, 9	co 7421	. . . . . 6 class (0[,]+∞)
11		vm	. . . . . . 7 setvar 𝑚
12	11	cv 1568	. . . . . 6 class 𝑚
13	6, 10, 12	wf 6535	. . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14		c0 4278	. . . . . . 7 class ∅
15	14, 12	cfv 6539	. . . . . 6 class (𝑚‘∅)
16	15, 7	wceq 1569	. . . . 5 wff (𝑚‘∅) = 0
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1568	. . . . . . . . 9 class 𝑥
19		com 7878	. . . . . . . . 9 class ω
20		cdom 8975	. . . . . . . . 9 class ≼
21	18, 19, 20	wbr 5102	. . . . . . . 8 wff 𝑥 ≼ ω
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1568	. . . . . . . . 9 class 𝑦
24	22, 18, 23	wdisj 5069	. . . . . . . 8 wff Disj 𝑦 ∈ 𝑥 𝑦
25	21, 24	wa 401	. . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)
26	18	cuni 4866	. . . . . . . . 9 class ∪ 𝑥
27	26, 12	cfv 6539	. . . . . . . 8 class (𝑚‘∪ 𝑥)
28	23, 12	cfv 6539	. . . . . . . . 9 class (𝑚‘𝑦)
29	18, 28, 22	cesum 34706	. . . . . . . 8 class Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
30	27, 29	wceq 1569	. . . . . . 7 wff (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
31	25, 30	wi 4	. . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
32	6	cpw 4556	. . . . . 6 class 𝒫 𝑠
33	31, 17, 32	wral 3076	. . . . 5 wff ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
34	13, 16, 33	w3a 1103	. . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))
35	34, 11	cab 2738	. . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}
36	2, 5, 35	cmpt 5185	. 2 class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
37	1, 36	wceq 1569	1 wff measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

This definition is used by:  measbase  34877  measval  34878  ismeas  34879  isrnmeas  34880