Theorem bor1sal

Description: The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	bor1sal.t	⊢ 𝐽 = ( topGen ‘ ran (,) )
	bor1sal.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
Assertion	bor1sal	⊢ 𝐵 ∈ SAlg

Proof

Step	Hyp	Ref	Expression
1		bor1sal.t	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		bor1sal.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
3		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
4	1 3	eqeltri	⊢ 𝐽 ∈ Top
5	4	a1i	⊢ ( ⊤ → 𝐽 ∈ Top )
6	5 2	salgencld	⊢ ( ⊤ → 𝐵 ∈ SAlg )
7	6	mptru	⊢ 𝐵 ∈ SAlg