Metamath Proof Explorer

Theorem rrxunitopnfi

Description: The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Assertion	rrxunitopnfi	$⊢ X \in Fin \to ⋃ TopOpen (X) = ℝ^{X}$

Step	Hyp	Ref	Expression
1		eqidd	$⊢ X \in Fin \to ℝ^{X} = ℝ^{X}$
2		eqid	$⊢ TopOpen (X) = TopOpen (X)$
3	2	rrxtoponfi	$⊢ X \in Fin \to TopOpen (X) \in TopOn (ℝ^{X})$
4		toponuni	$⊢ TopOpen (X) \in TopOn (ℝ^{X}) \to ℝ^{X} = ⋃ TopOpen (X)$
5	3 4	syl	$⊢ X \in Fin \to ℝ^{X} = ⋃ TopOpen (X)$
6	1 5	eqtr2d	$⊢ X \in Fin \to ⋃ TopOpen (X) = ℝ^{X}$