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		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
4		eqid	⊢ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) = ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
5	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
6		df-ii	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
7	4 5 6	metrest	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( 𝐽 ↾t ( 0 [,] 1 ) ) = II )
8	2 3 7	mp2an	⊢ ( 𝐽 ↾t ( 0 [,] 1 ) ) = II
9	8	eqcomi	⊢ II = ( 𝐽 ↾t ( 0 [,] 1 ) )