Metamath Proof Explorer

Theorem rrxtopn0

Description: The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion rrxtopn0 ⊢ TopOpen ⁡ ∅ = 𝒫 ∅

Proof

Step Hyp Ref Expression
1 0fin ⊢ ∅ ∈ Fin
2 eqid ⊢ TopOpen ⁡ ∅ = TopOpen ⁡ ∅
3 2 rrxtoponfi ⊢ ∅ ∈ Fin → TopOpen ⁡ ∅ ∈ TopOn ⁡ ℝ ∅
4 1 3 ax-mp ⊢ TopOpen ⁡ ∅ ∈ TopOn ⁡ ℝ ∅
5 reex ⊢ ℝ ∈ V
6 mapdm0 ⊢ ℝ ∈ V → ℝ ∅ = ∅
7 5 6 ax-mp ⊢ ℝ ∅ = ∅
8 7 fveq2i ⊢ TopOn ⁡ ℝ ∅ = TopOn ⁡ ∅
9 4 8 eleqtri ⊢ TopOpen ⁡ ∅ ∈ TopOn ⁡ ∅
10 topsn ⊢ TopOpen ⁡ ∅ ∈ TopOn ⁡ ∅ → TopOpen ⁡ ∅ = 𝒫 ∅
11 9 10 ax-mp ⊢ TopOpen ⁡ ∅ = 𝒫 ∅