Theorem istoprelowl

Description: The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	istoprelowl.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
Assertion	istoprelowl	$$⊢\mathrm{topGen}\left(I\right)\in \mathrm{TopOn}\left(ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		istoprelowl.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
2	1	isbasisrelowl	$$⊢I\in \mathrm{TopBases}$$
3		tgtopon	$$⊢I\in \mathrm{TopBases}\to \mathrm{topGen}\left(I\right)\in \mathrm{TopOn}\left(\bigcup I\right)$$
4	1	icoreunrn	$$⊢ℝ=\bigcup I$$
5	4	eqcomi	$$⊢\bigcup I=ℝ$$
6	5	fveq2i	$$⊢\mathrm{TopOn}\left(\bigcup I\right)=\mathrm{TopOn}\left(ℝ\right)$$
7	3 6	eleqtrdi	$$⊢I\in \mathrm{TopBases}\to \mathrm{topGen}\left(I\right)\in \mathrm{TopOn}\left(ℝ\right)$$
8	2 7	ax-mp	$$⊢\mathrm{topGen}\left(I\right)\in \mathrm{TopOn}\left(ℝ\right)$$