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 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
3 ax-resscn 
 |-  RR C_ CC
4 2 3 sstri 
 |-  ( 0 [,] 1 ) C_ CC
5 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,] 1 ) C_ CC ) -> ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) ) )
6 1 4 5 mp2an 
 |-  ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) )
7 df-ii 
 |-  II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
8 7 mopntopon 
 |-  ( ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) e. ( *Met ` ( 0 [,] 1 ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
9 6 8 ax-mp 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )