Metamath Proof Explorer

Theorem sconnpconn

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

Ref Expression
Assertion sconnpconn 
|- ( J e. SConn -> J e. PConn )

Proof

Step Hyp Ref Expression
1 issconn 
 |-  ( J e. SConn <-> ( J e. PConn /\ A. f e. ( II Cn J ) ( ( f ` 0 ) = ( f ` 1 ) -> f ( ~=ph ` J ) ( ( 0 [,] 1 ) X. { ( f ` 0 ) } ) ) ) )
2 1 simplbi 
 |-  ( J e. SConn -> J e. PConn )