Metamath Proof Explorer

Theorem dmmeas

Description: The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018)

		Ref	Expression
	Assertion	dmmeas	\|- ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )

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	simpld	\|- ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )

Step

Hyp

Ref

Expression

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 ) ) ) ) )

simpld

 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )