Metamath Proof Explorer


Theorem opnssborel

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 𝐴 = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
opnssborel.b 𝐵 = ( SalGen ‘ 𝐴 )
Assertion opnssborel 𝐴𝐵

Proof

Step Hyp Ref Expression
1 opnssborel.a 𝐴 = ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) )
2 opnssborel.b 𝐵 = ( SalGen ‘ 𝐴 )
3 1 fvexi 𝐴 ∈ V
4 2 sssalgen ( 𝐴 ∈ V → 𝐴𝐵 )
5 3 4 ax-mp 𝐴𝐵