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