Theorem dmvlsiga

Description: Lebesgue-measurable subsets of RR form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016) (Revised by Thierry Arnoux, 24-Oct-2016)

	Ref	Expression
Assertion	dmvlsiga	|- dom vol e. ( sigAlgebra ` RR )

Proof

Step	Hyp	Ref	Expression
1		pwssb	|- ( dom vol C_ ~P RR <-> A. x e. dom vol x C_ RR )
2		mblss	|- ( x e. dom vol -> x C_ RR )
3	1 2	mprgbir	|- dom vol C_ ~P RR
4		rembl	|- RR e. dom vol
5		cmmbl	|- ( x e. dom vol -> ( RR \ x ) e. dom vol )
6	5	rgen	|- A. x e. dom vol ( RR \ x ) e. dom vol
7		nnenom	|- NN ~~ _om
8	7	ensymi	|- _om ~~ NN
9		domentr	|- ( ( x ~<_ _om /\ _om ~~ NN ) -> x ~<_ NN )
10	8 9	mpan2	|- ( x ~<_ _om -> x ~<_ NN )
11		elpwi	|- ( x e. ~P dom vol -> x C_ dom vol )
12		dfss3	|- ( x C_ dom vol <-> A. y e. x y e. dom vol )
13	11 12	sylib	|- ( x e. ~P dom vol -> A. y e. x y e. dom vol )
14		iunmbl2	|- ( ( x ~<_ NN /\ A. y e. x y e. dom vol ) -> U_ y e. x y e. dom vol )
15	10 13 14	syl2anr	|- ( ( x e. ~P dom vol /\ x ~<_ _om ) -> U_ y e. x y e. dom vol )
16	15	ex	|- ( x e. ~P dom vol -> ( x ~<_ _om -> U_ y e. x y e. dom vol ) )
17		uniiun	|- U. x = U_ y e. x y
18	17	eleq1i	|- ( U. x e. dom vol <-> U_ y e. x y e. dom vol )
19	16 18	syl6ibr	|- ( x e. ~P dom vol -> ( x ~<_ _om -> U. x e. dom vol ) )
20	19	rgen	|- A. x e. ~P dom vol ( x ~<_ _om -> U. x e. dom vol )
21	4 6 20	3pm3.2i	|- ( RR e. dom vol /\ A. x e. dom vol ( RR \ x ) e. dom vol /\ A. x e. ~P dom vol ( x ~<_ _om -> U. x e. dom vol ) )
22		reex	|- RR e. _V
23	22	pwex	|- ~P RR e. _V
24	23 3	ssexi	|- dom vol e. _V
25		issiga	|- ( dom vol e. _V -> ( dom vol e. ( sigAlgebra ` RR ) <-> ( dom vol C_ ~P RR /\ ( RR e. dom vol /\ A. x e. dom vol ( RR \ x ) e. dom vol /\ A. x e. ~P dom vol ( x ~<_ _om -> U. x e. dom vol ) ) ) ) )
26	24 25	ax-mp	|- ( dom vol e. ( sigAlgebra ` RR ) <-> ( dom vol C_ ~P RR /\ ( RR e. dom vol /\ A. x e. dom vol ( RR \ x ) e. dom vol /\ A. x e. ~P dom vol ( x ~<_ _om -> U. x e. dom vol ) ) ) )
27	3 21 26	mpbir2an	|- dom vol e. ( sigAlgebra ` RR )