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 (I)$
	Assertion	rrxtopon	$⊢ I \in V \to J \in TopOn ({Base}_{I})$

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