Theorem iiconn

Description: The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	iiconn	$$⊢\mathrm{II}\in \mathrm{Conn}$$

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		iccconn	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)\to \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]\in \mathrm{Conn}$$
5	2 3 4	mp2an	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right){\upharpoonright }_{𝑡}\left[0,1\right]\in \mathrm{Conn}$$
6	1 5	eqeltri	$$⊢\mathrm{II}\in \mathrm{Conn}$$