This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem perftop

Description: A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Assertion perftop ⊢ J ∈ Perf → J ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 isperf ⊢ J ∈ Perf ↔ J ∈ Top ∧ limPt ⁡ J ⁡ ⋃ J = ⋃ J
3 2 simplbi ⊢ J ∈ Perf → J ∈ Top