Metamath Proof Explorer


Theorem unidmvol

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

Proof

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