Theorem bor1sal

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

	Ref	Expression
Hypotheses	bor1sal.t	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	bor1sal.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
Assertion	bor1sal	$$⊢B\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		bor1sal.t	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		bor1sal.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
3		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
4	1 3	eqeltri	$$⊢J\in \mathrm{Top}$$
5	4	a1i	$$⊢\top \to J\in \mathrm{Top}$$
6	5 2	salgencld	$$⊢\top \to B\in \mathrm{SAlg}$$
7	6	mptru	$$⊢B\in \mathrm{SAlg}$$