Theorem retps

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

	Ref	Expression
Hypothesis	retps.k	|- K = { <. ( Base ` ndx ) , RR >. , <. ( TopSet ` ndx ) , ( topGen ` ran (,) ) >. }
Assertion	retps	|- K e. TopSp

Proof

Step	Hyp	Ref	Expression
1		retps.k	|- K = { <. ( Base ` ndx ) , RR >. , <. ( TopSet ` ndx ) , ( topGen ` ran (,) ) >. }
2		uniretop	|- RR = U. ( topGen ` ran (,) )
3		retop	|- ( topGen ` ran (,) ) e. Top
4	1 2 3	eltpsi	|- K e. TopSp