Metamath Proof Explorer

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 e. Comp

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1re 
 |-  1 e. RR
3 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
4 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
5 3 4 icccmp 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> II e. Comp )
6 1 2 5 mp2an 
 |-  II e. Comp