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 e. U. ran sigAlgebra -> ( measures ` S ) = { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) -> m : S --> ( 0 [,] +oo ) )
2 1 ss2abi 
 |-  { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } C_ { m | m : S --> ( 0 [,] +oo ) }
3 ovex 
 |-  ( 0 [,] +oo ) e. _V
4 mapex 
 |-  ( ( S e. U. ran sigAlgebra /\ ( 0 [,] +oo ) e. _V ) -> { m | m : S --> ( 0 [,] +oo ) } e. _V )
5 3 4 mpan2 
 |-  ( S e. U. ran sigAlgebra -> { m | m : S --> ( 0 [,] +oo ) } e. _V )
6 ssexg 
 |-  ( ( { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } C_ { m | m : S --> ( 0 [,] +oo ) } /\ { m | m : S --> ( 0 [,] +oo ) } e. _V ) -> { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } e. _V )
7 2 5 6 sylancr 
 |-  ( S e. U. ran sigAlgebra -> { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } e. _V )
8 feq2 
 |-  ( s = S -> ( m : s --> ( 0 [,] +oo ) <-> m : S --> ( 0 [,] +oo ) ) )
9 pweq 
 |-  ( s = S -> ~P s = ~P S )
10 9 raleqdv 
 |-  ( s = S -> ( A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) )
11 8 10 3anbi13d 
 |-  ( s = S -> ( ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) <-> ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) ) )
12 11 abbidv 
 |-  ( s = S -> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } = { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )
13 df-meas 
 |-  measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )
14 12 13 fvmptg 
 |-  ( ( S e. U. ran sigAlgebra /\ { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } e. _V ) -> ( measures ` S ) = { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )
15 7 14 mpdan 
 |-  ( S e. U. ran sigAlgebra -> ( measures ` S ) = { m | ( m : S --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )