Theorem brsiga

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

	Ref	Expression
Assertion	brsiga	$$⊢{𝔅}_{ℝ}\in 𝛔\left[\mathrm{Top}\right]$$

Proof

Step	Hyp	Ref	Expression
1		df-brsiga	$$⊢{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
2		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
3		df-sigagen	$$⊢𝛔=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}\right)$$
4	3	funmpt2	$$⊢\mathrm{Fun}𝛔$$
5		fvex	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{V}$$
6		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)$$
7		elrnsiga	$$⊢𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \mathrm{sigAlgebra}\left(\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
8	5 6 7	mp2b	$$⊢𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
9		0elsiga	$$⊢𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \varnothing \in 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
10		elfvdm	$$⊢\varnothing \in 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{dom}𝛔$$
11	8 9 10	mp2b	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{dom}𝛔$$
12		funfvima	$$⊢\left(\mathrm{Fun}𝛔\wedge \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{dom}𝛔\right)\to \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in 𝛔\left[\mathrm{Top}\right]\right)$$
13	4 11 12	mp2an	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to 𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in 𝛔\left[\mathrm{Top}\right]$$
14	2 13	ax-mp	$$⊢𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\in 𝛔\left[\mathrm{Top}\right]$$
15	1 14	eqeltri	$$⊢{𝔅}_{ℝ}\in 𝛔\left[\mathrm{Top}\right]$$