# Metamath Proof Explorer

## 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)$