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	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{V}$$
2		sigagensiga	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{V}\to 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
3	1 2	ax-mp	$$⊢𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
4		df-brsiga	$$⊢{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
5		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
6	5	fveq2i	$$⊢\mathrm{sigAlgebra}\left(ℝ\right)=\mathrm{sigAlgebra}\left(\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
7	3 4 6	3eltr4i	$$⊢{𝔅}_{ℝ}\in \mathrm{sigAlgebra}\left(ℝ\right)$$