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 ) )