Metamath Proof Explorer

Theorem pconntop

Description: A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion pconntop 
|- ( J e. PConn -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 ispconn 
 |-  ( J e. PConn <-> ( J e. Top /\ A. x e. U. J A. y e. U. J E. f e. ( II Cn J ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
3 2 simplbi 
 |-  ( J e. PConn -> J e. Top )