Theorem dfii2

Description: Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	dfii2	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )

Proof

Step	Hyp	Ref	Expression
1		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
2		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
3		df-ii	⊢ II = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) )
4	2 3	resubmet	⊢ ( ( 0 [,] 1 ) ⊆ ℝ → II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) ) )
5	1 4	ax-mp	⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )