Theorem rrxtps

Description: Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Assertion	rrxtps	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		rrxngp	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ NrmGrp )
2		ngptps	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ NrmGrp → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
3	1 2	syl	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )