Theorem dmmeasal

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

	Ref	Expression
Hypotheses	dmmeasal.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	dmmeasal.s	$$⊢S=\mathrm{dom}M$$
Assertion	dmmeasal	$$⊢\phi \to S\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		dmmeasal.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		dmmeasal.s	$$⊢S=\mathrm{dom}M$$
3		ismea	$$⊢M\in \mathrm{Meas}\leftrightarrow \left(\left(\left(M:\mathrm{dom}M⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}M\in \mathrm{SAlg}\right)\wedge M\left(\varnothing \right)=0\right)\wedge \forall x\in 𝒫\mathrm{dom}M\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to M\left(\bigcup x\right)=\mathrm{sum^}\left({M\upharpoonright }_x\right)\right)\right)$$
4	1 3	sylib	$$⊢\phi \to \left(\left(\left(M:\mathrm{dom}M⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}M\in \mathrm{SAlg}\right)\wedge M\left(\varnothing \right)=0\right)\wedge \forall x\in 𝒫\mathrm{dom}M\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to M\left(\bigcup x\right)=\mathrm{sum^}\left({M\upharpoonright }_x\right)\right)\right)$$
5	4	simplld	$$⊢\phi \to \left(M:\mathrm{dom}M⟶\left[0,\mathrm{+\infty }\right]\wedge \mathrm{dom}M\in \mathrm{SAlg}\right)$$
6	5	simprd	$$⊢\phi \to \mathrm{dom}M\in \mathrm{SAlg}$$
7	2 6	eqeltrid	$$⊢\phi \to S\in \mathrm{SAlg}$$