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 elfvunirn 
 |-  ( M e. ( measures ` dom M ) -> M e. U. ran measures )
8 6 7 impbii 
 |-  ( M e. U. ran measures <-> M e. ( measures ` dom M ) )