Theorem iisconn

Description: The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Assertion	iisconn	$$⊢\mathrm{II}\in \mathrm{SConn}$$

Proof

Step	Hyp	Ref	Expression
1		dfii2	$$⊢\mathrm{II}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]$$
2		0re	$$⊢0\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4		iccsconn	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]\in \mathrm{SConn}$$
5	2 3 4	mp2an	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]\in \mathrm{SConn}$$
6	1 5	eqeltri	$$⊢\mathrm{II}\in \mathrm{SConn}$$