Metamath Proof Explorer

Theorem rrxtop

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

Ref Expression
Hypothesis rrxtop.1 
|- J = ( TopOpen ` ( RR^ ` I ) )
Assertion rrxtop 
|- ( I e. V -> J e. Top )

Proof

Step Hyp Ref Expression
1 rrxtop.1 
 |-  J = ( TopOpen ` ( RR^ ` I ) )
2 rrxtps 
 |-  ( I e. V -> ( RR^ ` I ) e. TopSp )
3 1 tpstop 
 |-  ( ( RR^ ` I ) e. TopSp -> J e. Top )
4 2 3 syl 
 |-  ( I e. V -> J e. Top )