Metamath Proof Explorer

Theorem perftop

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

Ref Expression
Assertion perftop 
|- ( J e. Perf -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 isperf 
 |-  ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` U. J ) = U. J ) )
3 2 simplbi 
 |-  ( J e. Perf -> J e. Top )