Metamath Proof Explorer

Definition df-meas

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

Ref Expression
Assertion df-meas ⊢ measures = s ∈ ⋃ ran ⁡ sigAlgebra ⟼ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmeas class measures
1 vs setvar s
2 csiga class sigAlgebra
3 2 crn class ran ⁡ sigAlgebra
4 3 cuni class ⋃ ran ⁡ sigAlgebra
5 vm setvar m
6 5 cv setvar m
7 1 cv setvar s
8 cc0 class 0
9 cicc class .
10 cpnf class +∞
11 8 10 9 co class 0 +∞
12 7 11 6 wf wff m : s ⟶ 0 +∞
13 c0 class ∅
14 13 6 cfv class m ⁡ ∅
15 14 8 wceq wff m ⁡ ∅ = 0
16 vx setvar x
17 7 cpw class 𝒫 s
18 16 cv setvar x
19 cdom class ≼
20 com class ω
21 18 20 19 wbr wff x ≼ ω
22 vy setvar y
23 22 cv setvar y
24 22 18 23 wdisj wff Disj y ∈ x y
25 21 24 wa wff x ≼ ω ∧ Disj y ∈ x y
26 18 cuni class ⋃ x
27 26 6 cfv class m ⁡ ⋃ x
28 23 6 cfv class m ⁡ y
29 18 28 22 cesum class ∑ * y ∈ x m ⁡ y
30 27 29 wceq wff m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
31 25 30 wi wff x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
32 31 16 17 wral wff ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
33 12 15 32 w3a wff m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
34 33 5 cab class m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
35 1 4 34 cmpt class s ∈ ⋃ ran ⁡ sigAlgebra ⟼ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
36 0 35 wceq wff measures = s ∈ ⋃ ran ⁡ sigAlgebra ⟼ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y