Description: The union of the Lebesgue measurable sets is RR . (Contributed by Thierry Arnoux, 30-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | unidmvol | |- U. dom vol = RR |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unissb | |- ( U. dom vol C_ RR <-> A. x e. dom vol x C_ RR ) |
|
2 | mblss | |- ( x e. dom vol -> x C_ RR ) |
|
3 | 1 2 | mprgbir | |- U. dom vol C_ RR |
4 | rembl | |- RR e. dom vol |
|
5 | unissel | |- ( ( U. dom vol C_ RR /\ RR e. dom vol ) -> U. dom vol = RR ) |
|
6 | 3 4 5 | mp2an | |- U. dom vol = RR |