Theorem ioontr

Description: The interior of an interval in the standard topology on RR is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	ioontr	$$⊢\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\left(A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iooretop	$$⊢\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
3		ioossre	$$⊢\left(A,B\right)\subseteq ℝ$$
4		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5	4	isopn3	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge \left(A,B\right)\subseteq ℝ\right)\to \left(\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\left(A,B\right)\right)$$
6	2 3 5	mp2an	$$⊢\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\left(A,B\right)$$
7	1 6	mpbi	$$⊢\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\left(A,B\right)$$