Metamath Proof Explorer


Theorem dmvolsal

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

Ref Expression
Assertion dmvolsal dom vol SAlg

Proof

Step Hyp Ref Expression
1 reex V
2 1 pwex 𝒫 V
3 dmvolss dom vol 𝒫
4 2 3 ssexi dom vol V
5 4 a1i dom vol V
6 0mbl dom vol
7 6 a1i dom vol
8 unidmvol dom vol =
9 8 eqcomi = dom vol
10 cmmbl y dom vol y dom vol
11 10 adantl y dom vol y dom vol
12 ffvelrn e : dom vol n e n dom vol
13 12 ralrimiva e : dom vol n e n dom vol
14 iunmbl n e n dom vol n e n dom vol
15 13 14 syl e : dom vol n e n dom vol
16 15 adantl e : dom vol n e n dom vol
17 5 7 9 11 16 issalnnd dom vol SAlg
18 17 mptru dom vol SAlg