Metamath Proof Explorer

Theorem iitopon

Description: The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion iitopon 
|- II e. ( TopOn ` ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
2 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
3 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,] 1 ) C_ CC ) -> ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) ) )
4 1 2 3 mp2an 
 |-  ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) )
5 df-ii 
 |-  II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
6 5 mopntopon 
 |-  ( ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
7 4 6 ax-mp 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )