# Metamath Proof Explorer

## Theorem dfii3

Description: Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis dfii3.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion dfii3 ${⊢}\mathrm{II}={J}{↾}_{𝑡}\left[0,1\right]$

### Proof

Step Hyp Ref Expression
1 dfii3.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
3 unitssre ${⊢}\left[0,1\right]\subseteq ℝ$
4 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 3 4 sstri ${⊢}\left[0,1\right]\subseteq ℂ$
6 eqid ${⊢}{\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}={\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}$
7 1 cnfldtopn ${⊢}{J}=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
8 df-ii ${⊢}\mathrm{II}=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)↾}_{\left(\left[0,1\right]×\left[0,1\right]\right)}\right)$
9 6 7 8 metrest ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge \left[0,1\right]\subseteq ℂ\right)\to {J}{↾}_{𝑡}\left[0,1\right]=\mathrm{II}$
10 2 5 9 mp2an ${⊢}{J}{↾}_{𝑡}\left[0,1\right]=\mathrm{II}$
11 10 eqcomi ${⊢}\mathrm{II}={J}{↾}_{𝑡}\left[0,1\right]$