Metamath Proof Explorer


Theorem brsigasspwrn

Description: The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017)

Ref Expression
Assertion brsigasspwrn
|- BrSiga C_ ~P RR

Proof

Step Hyp Ref Expression
1 brsigarn
 |-  BrSiga e. ( sigAlgebra ` RR )
2 sigasspw
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga C_ ~P RR )
3 1 2 ax-mp
 |-  BrSiga C_ ~P RR