Theorem sconnpconn

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

	Ref	Expression
Assertion	sconnpconn	$$⊢J\in \mathrm{SConn}\to J\in \mathrm{PConn}$$

Proof

Step	Hyp	Ref	Expression
1		issconn	$$⊢J\in \mathrm{SConn}\leftrightarrow \left(J\in \mathrm{PConn}\wedge \forall f\in \left(\mathrm{II}\mathrm{Cn}J\right)\left(f\left(0\right)=f\left(1\right)\to f{\simeq }_{\mathrm{ph}}\left(J\right)\left(\left[0,1\right]\times \left\{f\left(0\right)\right\}\right)\right)\right)$$
2	1	simplbi	$$⊢J\in \mathrm{SConn}\to J\in \mathrm{PConn}$$