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	⊢ 𝔅ℝ ⊆ 𝒫 ℝ

Proof

Step	Hyp	Ref	Expression
1		brsigarn	⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
2		sigasspw	⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ⊆ 𝒫 ℝ )
3	1 2	ax-mp	⊢ 𝔅ℝ ⊆ 𝒫 ℝ