Theorem iooborel

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

	Ref	Expression
Hypotheses	iooborel.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	iooborel.2	$$⊢B=\mathrm{SalGen}\left(J\right)$$
Assertion	iooborel	$$⊢\left(A,C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		iooborel.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		iooborel.2	$$⊢B=\mathrm{SalGen}\left(J\right)$$
3		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
4	1 3	eqeltri	$$⊢J\in \mathrm{Top}$$
5	2	sssalgen	$$⊢J\in \mathrm{Top}\to J\subseteq B$$
6	4 5	ax-mp	$$⊢J\subseteq B$$
7		iooretop	$$⊢\left(A,C\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
8	7 1	eleqtrri	$$⊢\left(A,C\right)\in J$$
9	6 8	sselii	$$⊢\left(A,C\right)\in B$$