Metamath Proof Explorer

Theorem cmptop

Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009)

Ref Expression
Assertion cmptop 
|- ( J e. Comp -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 iscmp 
 |-  ( J e. Comp <-> ( J e. Top /\ A. r e. ~P J ( U. J = U. r -> E. s e. ( ~P r i^i Fin ) U. J = U. s ) ) )
3 2 simplbi 
 |-  ( J e. Comp -> J e. Top )