Description: Open sets of a generalized real Euclidean space are Borel sets (notice that this theorem is even more general, because X is not required to be a set). (Contributed by Glauco Siliprandi, 3-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | opnssborel.a | |- A = ( TopOpen ` ( RR^ ` X ) ) |
|
| opnssborel.b | |- B = ( SalGen ` A ) |
||
| Assertion | opnssborel | |- A C_ B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opnssborel.a | |- A = ( TopOpen ` ( RR^ ` X ) ) |
|
| 2 | opnssborel.b | |- B = ( SalGen ` A ) |
|
| 3 | 1 | fvexi | |- A e. _V |
| 4 | 2 | sssalgen | |- ( A e. _V -> A C_ B ) |
| 5 | 3 4 | ax-mp | |- A C_ B |