Metamath Proof Explorer


Theorem measval

Description: The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016)

Ref Expression
Assertion measval S ran sigAlgebra measures S = m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y

Proof

Step Hyp Ref Expression
1 simp1 m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y m : S 0 +∞
2 1 ss2abi m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y m | m : S 0 +∞
3 ovex 0 +∞ V
4 mapex S ran sigAlgebra 0 +∞ V m | m : S 0 +∞ V
5 3 4 mpan2 S ran sigAlgebra m | m : S 0 +∞ V
6 ssexg m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y m | m : S 0 +∞ m | m : S 0 +∞ V m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y V
7 2 5 6 sylancr S ran sigAlgebra m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y V
8 feq2 s = S m : s 0 +∞ m : S 0 +∞
9 pweq s = S 𝒫 s = 𝒫 S
10 9 raleqdv s = S x 𝒫 s x ω Disj y x y m x = * y x m y x 𝒫 S x ω Disj y x y m x = * y x m y
11 8 10 3anbi13d s = S m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y
12 11 abbidv s = S m | m : s 0 +∞ m = 0 x 𝒫 s x ω Disj y x y m x = * y x m y = m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y
13 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
14 12 13 fvmptg S ran sigAlgebra m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y V measures S = m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y
15 7 14 mpdan S ran sigAlgebra measures S = m | m : S 0 +∞ m = 0 x 𝒫 S x ω Disj y x y m x = * y x m y