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 e. Fin -> U. ( TopOpen ` ( RR^ ` X ) ) = ( RR ^m X ) )

Proof

Step	Hyp	Ref	Expression
1		eqidd	|- ( X e. Fin -> ( RR ^m X ) = ( RR ^m X ) )
2		eqid	|- ( TopOpen ` ( RR^ ` X ) ) = ( TopOpen ` ( RR^ ` X ) )
3	2	rrxtoponfi	|- ( X e. Fin -> ( TopOpen ` ( RR^ ` X ) ) e. ( TopOn ` ( RR ^m X ) ) )
4		toponuni	|- ( ( TopOpen ` ( RR^ ` X ) ) e. ( TopOn ` ( RR ^m X ) ) -> ( RR ^m X ) = U. ( TopOpen ` ( RR^ ` X ) ) )
5	3 4	syl	|- ( X e. Fin -> ( RR ^m X ) = U. ( TopOpen ` ( RR^ ` X ) ) )
6	1 5	eqtr2d	|- ( X e. Fin -> U. ( TopOpen ` ( RR^ ` X ) ) = ( RR ^m X ) )