Theorem bor1sal

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

	Ref	Expression
Hypotheses	bor1sal.t	|- J = ( topGen ` ran (,) )
	bor1sal.b	|- B = ( SalGen ` J )
Assertion	bor1sal	|- B e. SAlg

Proof

Step	Hyp	Ref	Expression
1		bor1sal.t	|- J = ( topGen ` ran (,) )
2		bor1sal.b	|- B = ( SalGen ` J )
3		retop	|- ( topGen ` ran (,) ) e. Top
4	1 3	eqeltri	|- J e. Top
5	4	a1i	|- ( T. -> J e. Top )
6	5 2	salgencld	|- ( T. -> B e. SAlg )
7	6	mptru	|- B e. SAlg