Theorem iicmp

Description: The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Jun-2014)

	Ref	Expression
Assertion	iicmp	$$⊢\mathrm{II}\in \mathrm{Comp}$$

Proof

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