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

Metamath Proof Explorer

Theorem retopon

Description: The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015)

		Ref	Expression
	Assertion	retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$

Step	Hyp	Ref	Expression
1		retop	$⊢ topGen (ran (.)) \in Top$
2		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
3	2	toptopon	$⊢ topGen (ran (.)) \in Top \leftrightarrow topGen (ran (.)) \in TopOn (ℝ)$
4	1 3	mpbi	$⊢ topGen (ran (.)) \in TopOn (ℝ)$