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 ∈ Top

Proof

Step Hyp Ref Expression
1 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
2 1 topontopi ⊢ II ∈ Top