Description: An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iooborel.1 | ||
iooborel.2 | |||
Assertion | iooborel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iooborel.1 | ||
2 | iooborel.2 | ||
3 | retop | ||
4 | 1 3 | eqeltri | |
5 | 2 | sssalgen | |
6 | 4 5 | ax-mp | |
7 | iooretop | ||
8 | 7 1 | eleqtrri | |
9 | 6 8 | sselii |