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	$$⊢{𝔅}_{ℝ}\subseteq 𝒫ℝ$$

Proof

Step	Hyp	Ref	Expression
1		brsigarn	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$$
2		sigasspw	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)\to {𝔅}_{ℝ}\subseteq 𝒫ℝ$$
3	1 2	ax-mp	$$⊢{𝔅}_{ℝ}\subseteq 𝒫ℝ$$