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 unitsscn ⊢ 0 1 ⊆ ℂ
3 xmetres2 ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 0 1 ⊆ ℂ → abs ∘ − ↾ 0 1 × 0 1 ∈ ∞Met ⁡ 0 1
4 1 2 3 mp2an ⊢ abs ∘ − ↾ 0 1 × 0 1 ∈ ∞Met ⁡ 0 1
5 df-ii ⊢ II = MetOpen ⁡ abs ∘ − ↾ 0 1 × 0 1
6 5 mopntopon ⊢ abs ∘ − ↾ 0 1 × 0 1 ∈ ∞Met ⁡ 0 1 → II ∈ TopOn ⁡ 0 1
7 4 6 ax-mp ⊢ II ∈ TopOn ⁡ 0 1