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

Metamath Proof Explorer

Theorem iitopon

Description: The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
2 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
3 ax-resscn ⊢ ℝ ⊆ ℂ
4 2 3 sstri ⊢ ( 0 [,] 1 ) ⊆ ℂ
5 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) )
6 1 4 5 mp2an ⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) )
7 df-ii ⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
8 7 mopntopon ⊢ ( ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) ∈ ( ∞Met ‘ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
9 6 8 ax-mp ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )