Theorem uniretop

Description: The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007)

	Ref	Expression
Assertion	uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )

Proof

Step	Hyp	Ref	Expression
1		unirnioo	⊢ ℝ = ∪ ran (,)
2		retopbas	⊢ ran (,) ∈ TopBases
3		unitg	⊢ ( ran (,) ∈ TopBases → ∪ ( topGen ‘ ran (,) ) = ∪ ran (,) )
4	2 3	ax-mp	⊢ ∪ ( topGen ‘ ran (,) ) = ∪ ran (,)
5	1 4	eqtr4i	⊢ ℝ = ∪ ( topGen ‘ ran (,) )