Metamath Proof Explorer

Theorem measbasedom

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

Ref Expression
Assertion measbasedom 
|- ( M e. U. ran measures <-> M e. ( measures ` dom M ) )

Proof

Step Hyp Ref Expression
1 isrnmeas 
 |-  ( M e. U. ran measures -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
2 1 simprd 
 |-  ( M e. U. ran measures -> ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
3 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
4 ismeas 
 |-  ( dom M e. U. ran sigAlgebra -> ( M e. ( measures ` dom M ) <-> ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
5 3 4 syl 
 |-  ( M e. U. ran measures -> ( M e. ( measures ` dom M ) <-> ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
6 2 5 mpbird 
 |-  ( M e. U. ran measures -> M e. ( measures ` dom M ) )
7 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 ) ) ) } )
8 7 funmpt2 
 |-  Fun measures
9 elunirn2 
 |-  ( ( Fun measures /\ M e. ( measures ` dom M ) ) -> M e. U. ran measures )
10 8 9 mpan 
 |-  ( M e. ( measures ` dom M ) -> M e. U. ran measures )
11 6 10 impbii 
 |-  ( M e. U. ran measures <-> M e. ( measures ` dom M ) )