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