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 ⁡ I
Assertion rrxtop ⊢ I ∈ V → J ∈ Top

Proof

Step Hyp Ref Expression
1 rrxtop.1 ⊢ J = TopOpen ⁡ I
2 rrxtps ⊢ I ∈ V → I ∈ TopSp
3 1 tpstop ⊢ I ∈ TopSp → J ∈ Top
4 2 3 syl ⊢ I ∈ V → J ∈ Top