Theorem pconntop

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

	Ref	Expression
Assertion	pconntop	$$⊢J\in \mathrm{PConn}\to J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	ispconn	$$⊢J\in \mathrm{PConn}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in \bigcup J\forall y\in \bigcup J\exists f\in \left(\mathrm{II}\mathrm{Cn}J\right)\left(f\left(0\right)=x\wedge f\left(1\right)=y\right)\right)$$
3	2	simplbi	$$⊢J\in \mathrm{PConn}\to J\in \mathrm{Top}$$