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 (msup)$
	Assertion	rrxtoponfi	$⊢ I \in Fin \to J \in TopOn (ℝ^{I})$

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