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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dfii3 II = ( 𝐽 ↾t ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 dfii3.1 ⊢ 𝐽 = ( 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 ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
8 df-ii ⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
9 6 7 8 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( 𝐽 ↾t ( 0 [,] 1 ) ) = II )
10 2 5 9 mp2an ⊢ ( 𝐽 ↾t ( 0 [,] 1 ) ) = II
11 10 eqcomi ⊢ II = ( 𝐽 ↾t ( 0 [,] 1 ) )