Theorem isbasisrelowl

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

	Ref	Expression
Hypothesis	isbasisrelowl.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
Assertion	isbasisrelowl	$$⊢I\in \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		isbasisrelowl.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
2		df-ico	$$⊢\left[.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
3	2	ixxex	$$⊢\left[.\right)\in \mathrm{V}$$
4		imaexg	$$⊢\left[.\right)\in \mathrm{V}\to \left[.\right)\left[{ℝ}^2\right]\in \mathrm{V}$$
5	3 4	ax-mp	$$⊢\left[.\right)\left[{ℝ}^2\right]\in \mathrm{V}$$
6	1 5	eqeltri	$$⊢I\in \mathrm{V}$$
7	1	icoreclin	$$⊢\left(x\in I\wedge y\in I\right)\to x\cap y\in I$$
8	7	rgen2	$$⊢\forall x\in I\forall y\in Ix\cap y\in I$$
9		fiinbas	$$⊢\left(I\in \mathrm{V}\wedge \forall x\in I\forall y\in Ix\cap y\in I\right)\to I\in \mathrm{TopBases}$$
10	6 8 9	mp2an	$$⊢I\in \mathrm{TopBases}$$