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	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbrsiga	⊢ 𝔅ℝ
1		csigagen	⊢ sigaGen
2		ctg	⊢ topGen
3		cioo	⊢ (,)
4	3	crn	⊢ ran (,)
5	4 2	cfv	⊢ ( topGen ‘ ran (,) )
6	5 1	cfv	⊢ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
7	0 6	wceq	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )