Theorem rrxtoponfi

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

	Ref	Expression
Hypothesis	rrxtopfi.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	rrxtoponfi	⊢ ( 𝐼 ∈ Fin → 𝐽 ∈ ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxtopfi.1	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
2	1	rrxtopon	⊢ ( 𝐼 ∈ Fin → 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
3		id	⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
4		eqid	⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
5		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
6	3 4 5	rrxbasefi	⊢ ( 𝐼 ∈ Fin → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
7	6	fveq2d	⊢ ( 𝐼 ∈ Fin → ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) = ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) )
8	2 7	eleqtrd	⊢ ( 𝐼 ∈ Fin → 𝐽 ∈ ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) )