Theorem dmmeasal

Description: The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	dmmeasal.m	|- ( ph -> M e. Meas )
	dmmeasal.s	|- S = dom M
Assertion	dmmeasal	|- ( ph -> S e. SAlg )

Proof

Step	Hyp	Ref	Expression
1		dmmeasal.m	|- ( ph -> M e. Meas )
2		dmmeasal.s	|- S = dom M
3		ismea	|- ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
4	1 3	sylib	|- ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
5	4	simplld	|- ( ph -> ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) )
6	5	simprd	|- ( ph -> dom M e. SAlg )
7	2 6	eqeltrid	|- ( ph -> S e. SAlg )