Metamath Proof Explorer

Theorem dfii5

Description: The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion dfii5 
|- II = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
2 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
3 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
4 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
5 3 4 xrrest 
 |-  ( ( 0 [,] 1 ) C_ RR -> ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) ) )
6 2 5 ax-mp 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
7 ordtresticc 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] 1 ) ) = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
8 1 6 7 3eqtr2i 
 |-  II = ( ordTop ` ( <_ i^i ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )