Metamath Proof Explorer

Theorem rrxtop

Description: The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Hypothesis	rrxtop.1	$⊢ J = TopOpen (msup)$
	Assertion	rrxtop	$⊢ I \in V \to J \in Top$

Step	Hyp	Ref	Expression
1		rrxtop.1	$⊢ J = TopOpen (msup)$
2		rrxtps	$⊢ I \in V \to msup \in TopSp$
3	1	tpstop	$⊢ msup \in TopSp \to J \in Top$
4	2 3	syl	$⊢ I \in V \to J \in Top$