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 ) )