Metamath Proof Explorer


Theorem iooborel

Description: An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses iooborel.1 J = topGen ran .
iooborel.2 B = SalGen J
Assertion iooborel A C B

Proof

Step Hyp Ref Expression
1 iooborel.1 J = topGen ran .
2 iooborel.2 B = SalGen J
3 retop topGen ran . Top
4 1 3 eqeltri J Top
5 2 sssalgen J Top J B
6 4 5 ax-mp J B
7 iooretop A C topGen ran .
8 7 1 eleqtrri A C J
9 6 8 sselii A C B