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

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 = TopOpen ⁡ ℂ fld
Assertion dfii3 ⊢ II = J ↾ 𝑡 0 1

Proof

Step Hyp Ref Expression
1 dfii3.1 ⊢ J = TopOpen ⁡ ℂ fld
2 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
3 unitssre ⊢ 0 1 ⊆ ℝ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 3 4 sstri ⊢ 0 1 ⊆ ℂ
6 eqid ⊢ abs ∘ − ↾ 0 1 × 0 1 = abs ∘ − ↾ 0 1 × 0 1
7 1 cnfldtopn ⊢ J = MetOpen ⁡ abs ∘ −
8 df-ii ⊢ II = MetOpen ⁡ abs ∘ − ↾ 0 1 × 0 1
9 6 7 8 metrest ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 0 1 ⊆ ℂ → J ↾ 𝑡 0 1 = II
10 2 5 9 mp2an ⊢ J ↾ 𝑡 0 1 = II
11 10 eqcomi ⊢ II = J ↾ 𝑡 0 1