This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iitop

Description: The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iitop 
|- II e. Top

Proof

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