Metamath Proof Explorer

Theorem rrxtopon

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

		Ref	Expression
	Hypothesis	rrxtopon.1	$⊢ J = TopOpen (msup)$
	Assertion	rrxtopon	$⊢ I \in V \to J \in TopOn ({Base}_{msup})$

Step	Hyp	Ref	Expression
1		rrxtopon.1	$⊢ J = TopOpen (msup)$
2		rrxtps	$⊢ I \in V \to msup \in TopSp$
3		eqid	$⊢ {Base}_{msup} = {Base}_{msup}$
4	3 1	istps	$⊢ msup \in TopSp \leftrightarrow J \in TopOn ({Base}_{msup})$
5	2 4	sylib	$⊢ I \in V \to J \in TopOn ({Base}_{msup})$