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
	opnssborel.b	$$⊢B=\mathrm{SalGen}\left(A\right)$$
Assertion	opnssborel	$$⊢A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		opnssborel.a
2		opnssborel.b	$$⊢B=\mathrm{SalGen}\left(A\right)$$
3	1	fvexi	$$⊢A\in \mathrm{V}$$
4	2	sssalgen	$$⊢A\in \mathrm{V}\to A\subseteq B$$
5	3 4	ax-mp	$$⊢A\subseteq B$$