# Metamath Proof Explorer

## Theorem iitopon

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

Ref Expression
Assertion iitopon ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$

### Proof

Step Hyp Ref Expression
1 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
2 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
3 ax-resscn ${⊢}ℝ\subseteq ℂ$
4 2 3 sstri ${⊢}\left[0,1\right]\subseteq ℂ$
5 xmetres2 ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge \left[0,1\right]\subseteq ℂ\right)\to {\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{\infty Met}\left(\left[0,1\right]\right)$
6 1 4 5 mp2an ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{\infty Met}\left(\left[0,1\right]\right)$
7 df-ii ${⊢}\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$
8 7 mopntopon ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\in \mathrm{\infty Met}\left(\left[0,1\right]\right)\to \mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$
9 6 8 ax-mp ${⊢}\mathrm{II}\in \mathrm{TopOn}\left(\left[0,1\right]\right)$