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 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 ffvelrn
 |-  ( ( 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