Definition df-meas 34175

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 34174	. 2 class measures
2		vs	. . 3 setvar 𝑠
3		csiga 34087	. . . . 5 class sigAlgebra
4	3	crn 5684	. . . 4 class ran sigAlgebra
5	4	cuni 4905	. . 3 class ∪ ran sigAlgebra
6	2	cv 1539	. . . . . 6 class 𝑠
7		cc0 11151	. . . . . . 7 class 0
8		cpnf 11288	. . . . . . 7 class +∞
9		cicc 13386	. . . . . . 7 class [,]
10	7, 8, 9	co 7429	. . . . . 6 class (0[,]+∞)
11		vm	. . . . . . 7 setvar 𝑚
12	11	cv 1539	. . . . . 6 class 𝑚
13	6, 10, 12	wf 6555	. . . . 5 wff 𝑚:𝑠⟶(0[,]+∞)
14		c0 4332	. . . . . . 7 class ∅
15	14, 12	cfv 6559	. . . . . 6 class (𝑚‘∅)
16	15, 7	wceq 1540	. . . . 5 wff (𝑚‘∅) = 0
17		vx	. . . . . . . . . 10 setvar 𝑥
18	17	cv 1539	. . . . . . . . 9 class 𝑥
19		com 7883	. . . . . . . . 9 class ω
20		cdom 8979	. . . . . . . . 9 class ≼
21	18, 19, 20	wbr 5141	. . . . . . . 8 wff 𝑥 ≼ ω
22		vy	. . . . . . . . 9 setvar 𝑦
23	22	cv 1539	. . . . . . . . 9 class 𝑦
24	22, 18, 23	wdisj 5108	. . . . . . . 8 wff Disj 𝑦 ∈ 𝑥 𝑦
25	21, 24	wa 395	. . . . . . 7 wff (𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦)
26	18	cuni 4905	. . . . . . . . 9 class ∪ 𝑥
27	26, 12	cfv 6559	. . . . . . . 8 class (𝑚‘∪ 𝑥)
28	23, 12	cfv 6559	. . . . . . . . 9 class (𝑚‘𝑦)
29	18, 28, 22	cesum 34006	. . . . . . . 8 class Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
30	27, 29	wceq 1540	. . . . . . 7 wff (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)
31	25, 30	wi 4	. . . . . 6 wff ((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
32	6	cpw 4598	. . . . . 6 class 𝒫 𝑠
33	31, 17, 32	wral 3060	. . . . 5 wff ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦))
34	13, 16, 33	w3a 1087	. . . 4 wff (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))
35	34, 11	cab 2713	. . 3 class {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))}
36	2, 5, 35	cmpt 5223	. 2 class (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
37	1, 36	wceq 1540	1 wff measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})

This definition is referenced by:  measbase  34176  measval  34177  ismeas  34178  isrnmeas  34179