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 ` ( RR^ ` I ) )
Assertion	rrxtoponfi	|- ( I e. Fin -> J e. ( TopOn ` ( RR ^m I ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxtopfi.1	|- J = ( TopOpen ` ( RR^ ` I ) )
2	1	rrxtopon	|- ( I e. Fin -> J e. ( TopOn ` ( Base ` ( RR^ ` I ) ) ) )
3		id	|- ( I e. Fin -> I e. Fin )
4		eqid	|- ( RR^ ` I ) = ( RR^ ` I )
5		eqid	|- ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
6	3 4 5	rrxbasefi	|- ( I e. Fin -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
7	6	fveq2d	|- ( I e. Fin -> ( TopOn ` ( Base ` ( RR^ ` I ) ) ) = ( TopOn ` ( RR ^m I ) ) )
8	2 7	eleqtrd	|- ( I e. Fin -> J e. ( TopOn ` ( RR ^m I ) ) )