Theorem dfii4

Description: Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Hypothesis	dfii4.1	⊢ 𝐼 = ( ℂfld ↾s ( 0 [,] 1 ) )
Assertion	dfii4	⊢ II = ( TopOpen ‘ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dfii4.1	⊢ 𝐼 = ( ℂfld ↾s ( 0 [,] 1 ) )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	dfii3	⊢ II = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) )
4	1 2	resstopn	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,] 1 ) ) = ( TopOpen ‘ 𝐼 )
5	3 4	eqtri	⊢ II = ( TopOpen ‘ 𝐼 )