Theorem brsigarn

Description: The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	brsigarn	⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( topGen ‘ ran (,) ) ∈ V
2		sigagensiga	⊢ ( ( topGen ‘ ran (,) ) ∈ V → ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigAlgebra ‘ ∪ ( topGen ‘ ran (,) ) ) )
3	1 2	ax-mp	⊢ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ∈ ( sigAlgebra ‘ ∪ ( topGen ‘ ran (,) ) )
4		df-brsiga	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
5		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
6	5	fveq2i	⊢ ( sigAlgebra ‘ ℝ ) = ( sigAlgebra ‘ ∪ ( topGen ‘ ran (,) ) )
7	3 4 6	3eltr4i	⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )