Metamath Proof Explorer


Theorem sconntop

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

Ref Expression
Assertion sconntop JSConnJTop

Proof

Step Hyp Ref Expression
1 sconnpconn JSConnJPConn
2 pconntop JPConnJTop
3 1 2 syl JSConnJTop