This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfii3

Description: Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis dfii3.1 
|- J = ( TopOpen ` CCfld )
Assertion dfii3 
|- II = ( J |`t ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 dfii3.1 
 |-  J = ( TopOpen ` CCfld )
2 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
3 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
4 ax-resscn 
 |-  RR C_ CC
5 3 4 sstri 
 |-  ( 0 [,] 1 ) C_ CC
6 eqid 
 |-  ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) = ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) )
7 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
8 df-ii 
 |-  II = ( MetOpen ` ( ( abs o. - ) |` ( ( 0 [,] 1 ) X. ( 0 [,] 1 ) ) ) )
9 6 7 8 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( 0 [,] 1 ) C_ CC ) -> ( J |`t ( 0 [,] 1 ) ) = II )
10 2 5 9 mp2an 
 |-  ( J |`t ( 0 [,] 1 ) ) = II
11 10 eqcomi 
 |-  II = ( J |`t ( 0 [,] 1 ) )