Theorem retps

Description: The standard topological space on the reals. (Contributed by NM, 19-Oct-2012)

	Ref	Expression
Hypothesis	retps.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℝ⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)⟩\right\}$$
Assertion	retps	$$⊢K\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		retps.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℝ⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)⟩\right\}$$
2		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
4	1 2 3	eltpsi	$$⊢K\in \mathrm{TopSp}$$