Theorem dfii4

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

	Ref	Expression
Hypothesis	dfii4.1	|- I = ( CCfld |`s ( 0 [,] 1 ) )
Assertion	dfii4	|- II = ( TopOpen ` I )

Proof

Step	Hyp	Ref	Expression
1		dfii4.1	|- I = ( CCfld |`s ( 0 [,] 1 ) )
2		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3	2	dfii3	|- II = ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) )
4	1 2	resstopn	|- ( ( TopOpen ` CCfld ) |`t ( 0 [,] 1 ) ) = ( TopOpen ` I )
5	3 4	eqtri	|- II = ( TopOpen ` I )