Definition df-meas 31450

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 31449	. 2 class measures
2		vs	. . 3 setvar 𝑠
3		csiga 31362	. . . . 5 class sigAlgebra
4	3	crn 5551	. . . 4 class ran sigAlgebra
5	4	cuni 4832	. . 3 class ∪ ran sigAlgebra
6	2	cv 1532	. . . . . 6 class 𝑠
7		cc0 10531	. . . . . . 7 class 0
8		cpnf 10666	. . . . . . 7 class +∞
9		cicc 12735	. . . . . . 7 class [,]
10	7, 8, 9	co 7150	. . . . . 6 class (0[,]+∞)
11		vm	. . . . . . 7 setvar 𝑚
12	11	cv 1532	. . . . . 6 class 𝑚
13	6, 10, 12	wf 6346	. . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14		c0 4291	. . . . . . 7 class ∅
15	14, 12	cfv 6350	. . . . . 6 class (𝑚‘∅)
16	15, 7	wceq 1533	. . . . 5 wff (𝑚‘∅) = 0
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1532	. . . . . . . . 9 class 𝑥
19		com 7574	. . . . . . . . 9 class ω
20		cdom 8501	. . . . . . . . 9 class ≼
21	18, 19, 20	wbr 5059	. . . . . . . 8 wff 𝑥 ≼ ω
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1532	. . . . . . . . 9 class 𝑦
24	22, 18, 23	wdisj 5024	. . . . . . . 8 wff Disj 𝑦 ∈ 𝑥 𝑦
25	21, 24	wa 398	. . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)
26	18	cuni 4832	. . . . . . . . 9 class ∪ 𝑥
27	26, 12	cfv 6350	. . . . . . . 8 class (𝑚‘∪ 𝑥)
28	23, 12	cfv 6350	. . . . . . . . 9 class (𝑚‘𝑦)
29	18, 28, 22	cesum 31281	. . . . . . . 8 class Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
30	27, 29	wceq 1533	. . . . . . 7 wff (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
31	25, 30	wi 4	. . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
32	6	cpw 4539	. . . . . 6 class 𝒫 𝑠
33	31, 17, 32	wral 3138	. . . . 5 wff ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
34	13, 16, 33	w3a 1083	. . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))
35	34, 11	cab 2799	. . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}
36	2, 5, 35	cmpt 5139	. 2 class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
37	1, 36	wceq 1533	1 wff measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

This definition is referenced by:  measbase  31451  measval  31452  ismeas  31453  isrnmeas  31454  measbasedom  31456