Metamath Proof Explorer

Theorem iiuni

Description: The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Jan-2014)

Ref Expression
Assertion iiuni 
|- ( 0 [,] 1 ) = U. II

Proof

Step Hyp Ref Expression
1 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
2 1 toponunii 
 |-  ( 0 [,] 1 ) = U. II