Metamath Proof Explorer

Theorem rrxtopon

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

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

Proof

Step Hyp Ref Expression
1 rrxtopon.1 
 |-  J = ( TopOpen ` ( RR^ ` I ) )
2 rrxtps 
 |-  ( I e. V -> ( RR^ ` I ) e. TopSp )
3 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
4 3 1 istps 
 |-  ( ( RR^ ` I ) e. TopSp <-> J e. ( TopOn ` ( Base ` ( RR^ ` I ) ) ) )
5 2 4 sylib 
 |-  ( I e. V -> J e. ( TopOn ` ( Base ` ( RR^ ` I ) ) ) )