Theorem iooretop

Description: Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007)

	Ref	Expression
Assertion	iooretop	$$⊢\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		retopbas	$$⊢\mathrm{ran}\left(.\right)\in \mathrm{TopBases}$$
2		bastg	$$⊢\mathrm{ran}\left(.\right)\in \mathrm{TopBases}\to \mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	1 2	ax-mp	$$⊢\mathrm{ran}\left(.\right)\subseteq \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4		ioorebas	$$⊢\left(A,B\right)\in \mathrm{ran}\left(.\right)$$
5	3 4	sselii	$$⊢\left(A,B\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$