Metamath Proof Explorer

Theorem measbase

Description: The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measbase 
|- ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( M e. ( measures ` S ) -> S e. dom measures )
2 vex 
 |-  s e. _V
3 ovex 
 |-  ( 0 [,] +oo ) e. _V
4 mapex 
 |-  ( ( s e. _V /\ ( 0 [,] +oo ) e. _V ) -> { m | m : s --> ( 0 [,] +oo ) } e. _V )
5 2 3 4 mp2an 
 |-  { m | m : s --> ( 0 [,] +oo ) } e. _V
6 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 ) )
7 6 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 ) }
8 5 7 ssexi 
 |-  { 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
9 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 ) ) ) } )
10 8 9 dmmpti 
 |-  dom measures = U. ran sigAlgebra
11 1 10 eleqtrdi 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )