Theorem retopon

Description: The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Assertion	retopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\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	toptopon	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\leftrightarrow \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$
4	1 3	mpbi	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{TopOn}\left(ℝ\right)$$