Metamath Proof Explorer

Theorem rrxtoponfi

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

		Ref	Expression
	Hypothesis	rrxtopfi.1	$⊢ J = TopOpen (I)$
	Assertion	rrxtoponfi	$⊢ I \in Fin \to J \in TopOn (ℝ^{I})$

Step	Hyp	Ref	Expression
1		rrxtopfi.1	$⊢ J = TopOpen (I)$
2	1	rrxtopon	$⊢ I \in Fin \to J \in TopOn ({Base}_{I})$
3		id	$⊢ I \in Fin \to I \in Fin$
4		eqid	$⊢ I = I$
5		eqid	$⊢ {Base}_{I} = {Base}_{I}$
6	3 4 5	rrxbasefi	$⊢ I \in Fin \to {Base}_{I} = ℝ^{I}$
7	6	fveq2d	$⊢ I \in Fin \to TopOn ({Base}_{I}) = TopOn (ℝ^{I})$
8	2 7	eleqtrd	$⊢ I \in Fin \to J \in TopOn (ℝ^{I})$