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	⊢ II ∈ Comp

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		1re	⊢ 1 ∈ ℝ
3		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
4		dfii2	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
5	3 4	icccmp	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → II ∈ Comp )
6	1 2 5	mp2an	⊢ II ∈ Comp