Theorem rrxtop

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

	Ref	Expression
Hypothesis	rrxtop.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	rrxtop	⊢ ( 𝐼 ∈ 𝑉 → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		rrxtop.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
2		rrxtps	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
3	1	tpstop	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ TopSp → 𝐽 ∈ Top )
4	2 3	syl	⊢ ( 𝐼 ∈ 𝑉 → 𝐽 ∈ Top )