Definition df-brsiga 30786

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 𝐽 is the sigma-algebra generated by 𝐽, (sigaGen‘𝐽), so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)

Assertion

Ref	Expression
df-brsiga	⊢ 𝔅ℝ = (sigaGen‘(topGen‘ran (,)))

Detailed syntax breakdown of Definition df-brsiga

Step	Hyp	Ref	Expression
1		cbrsiga 30785	. 2 class 𝔅ℝ
2		cioo 12470	. . . . 5 class (,)
3	2	crn 5347	. . . 4 class ran (,)
4		ctg 16458	. . . 4 class topGen
5	3, 4	cfv 6127	. . 3 class (topGen‘ran (,))
6		csigagen 30742	. . 3 class sigaGen
7	5, 6	cfv 6127	. 2 class (sigaGen‘(topGen‘ran (,)))
8	1, 7	wceq 1656	1 wff 𝔅ℝ = (sigaGen‘(topGen‘ran (,)))

This definition is referenced by:  brsiga  30787  brsigarn  30788  unibrsiga  30790  elmbfmvol2  30870  dya2iocbrsiga  30878  dya2icobrsiga  30879  sxbrsiga  30893  rrvadd  31056  rrvmulc  31057  orrvcval4  31068  orrvcoel  31069  orrvccel  31070