Theorem dmvolsal

Description: Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	dmvolsal	|- dom vol e. SAlg

Proof

Step	Hyp	Ref	Expression
1		reex	|- RR e. _V
2	1	pwex	|- ~P RR e. _V
3		dmvolss	|- dom vol C_ ~P RR
4	2 3	ssexi	|- dom vol e. _V
5	4	a1i	|- ( T. -> dom vol e. _V )
6		0mbl	|- (/) e. dom vol
7	6	a1i	|- ( T. -> (/) e. dom vol )
8		unidmvol	|- U. dom vol = RR
9	8	eqcomi	|- RR = U. dom vol
10		cmmbl	|- ( y e. dom vol -> ( RR \ y ) e. dom vol )
11	10	adantl	|- ( ( T. /\ y e. dom vol ) -> ( RR \ y ) e. dom vol )
12		ffvelcdm	|- ( ( e : NN --> dom vol /\ n e. NN ) -> ( e ` n ) e. dom vol )
13	12	ralrimiva	|- ( e : NN --> dom vol -> A. n e. NN ( e ` n ) e. dom vol )
14		iunmbl	|- ( A. n e. NN ( e ` n ) e. dom vol -> U_ n e. NN ( e ` n ) e. dom vol )
15	13 14	syl	|- ( e : NN --> dom vol -> U_ n e. NN ( e ` n ) e. dom vol )
16	15	adantl	|- ( ( T. /\ e : NN --> dom vol ) -> U_ n e. NN ( e ` n ) e. dom vol )
17	5 7 9 11 16	issalnnd	|- ( T. -> dom vol e. SAlg )
18	17	mptru	|- dom vol e. SAlg