Definition df-brsiga

Description: A Borel Algebra is defined as a sigma-algebra generated by a topology. 'The' Borel sigma-algebra here refers to the sigma-algebra generated by the topology of open intervals on real numbers. The Borel algebra of a given topology J is the sigma-algebra generated by J , ( sigaGenJ ) , so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	df-brsiga	$$⊢{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbrsiga	$$class{𝔅}_{ℝ}$$
1		csigagen	$$class𝛔$$
2		ctg	$$class\mathrm{topGen}$$
3		cioo	$$class\left(.\right)$$
4	3	crn	$$class\mathrm{ran}\left(.\right)$$
5	4 2	cfv	$$class\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
6	5 1	cfv	$$class𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
7	0 6	wceq	$$wff{𝔅}_{ℝ}=𝛔\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$