Theorem retps

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

	Ref	Expression
Hypothesis	retps.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , ℝ ⟩ , ⟨ ( TopSet ‘ ndx ) , ( topGen ‘ ran (,) ) ⟩ }
Assertion	retps	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		retps.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , ℝ ⟩ , ⟨ ( TopSet ‘ ndx ) , ( topGen ‘ ran (,) ) ⟩ }
2		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
3		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
4	1 2 3	eltpsi	⊢ 𝐾 ∈ TopSp