Theorem rrxtopon

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

	Ref	Expression
Hypothesis	rrxtopon.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	rrxtopon	⊢ ( 𝐼 ∈ 𝑉 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxtopon.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
2		rrxtps	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
3		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
4	3 1	istps	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
5	2 4	sylib	⊢ ( 𝐼 ∈ 𝑉 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )