Theorem dmovnsal

Description: The domain of the Lebesgue measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	dmovnsal.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	dmovnsal.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
Assertion	dmovnsal	$$⊢\phi \to S\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		dmovnsal.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		dmovnsal.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3	1	vonmea	$$⊢\phi \to \mathrm{voln}\left(X\right)\in \mathrm{Meas}$$
4	3 2	dmmeasal	$$⊢\phi \to S\in \mathrm{SAlg}$$