Theorem perftop

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

	Ref	Expression
Assertion	perftop	⊢ ( 𝐽 ∈ Perf → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	isperf	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ ∪ 𝐽 ) = ∪ 𝐽 ) )
3	2	simplbi	⊢ ( 𝐽 ∈ Perf → 𝐽 ∈ Top )