Theorem reopn

Description: The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	reopn	$$⊢ℝ\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
2		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3	2	topopn	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\to ℝ\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
4	1 3	ax-mp	$$⊢ℝ\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$