Metamath Proof Explorer


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 SAlg

Proof

Step Hyp Ref Expression
1 bor1sal.t J = topGen ran .
2 bor1sal.b B = SalGen J
3 retop topGen ran . Top
4 1 3 eqeltri J Top
5 4 a1i J Top
6 5 2 salgencld B SAlg
7 6 mptru B SAlg