This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (.))$

Step	Hyp	Ref	Expression
1		unirnioo	$⊢ ℝ = ⋃ ran (.)$
2		retopbas	$⊢ ran (.) \in TopBases$
3		unitg	$⊢ ran (.) \in TopBases \to ⋃ topGen (ran (.)) = ⋃ ran (.)$
4	2 3	ax-mp	$⊢ ⋃ topGen (ran (.)) = ⋃ ran (.)$
5	1 4	eqtr4i	$⊢ ℝ = ⋃ topGen (ran (.))$