Metamath Proof Explorer

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 ) C_ RR
2 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
3 df-ii 
 |-  II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
4 2 3 resubmet 
 |-  ( ( 0 [,] 1 ) C_ RR -> II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
5 1 4 ax-mp 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )