Metamath Proof Explorer

Theorem cnfldtopn

Description: The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis cnfldtopn.1 
|- J = ( TopOpen ` CCfld )
Assertion cnfldtopn 
|- J = ( MetOpen ` ( abs o. - ) )

Proof

Step Hyp Ref Expression
1 cnfldtopn.1 
 |-  J = ( TopOpen ` CCfld )
2 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
3 eqid 
 |-  ( MetOpen ` ( abs o. - ) ) = ( MetOpen ` ( abs o. - ) )
4 3 mopntopon 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( MetOpen ` ( abs o. - ) ) e. ( TopOn ` CC ) )
5 cnfldbas 
 |-  CC = ( Base ` CCfld )
6 cnfldtset 
 |-  ( MetOpen ` ( abs o. - ) ) = ( TopSet ` CCfld )
7 5 6 topontopn 
 |-  ( ( MetOpen ` ( abs o. - ) ) e. ( TopOn ` CC ) -> ( MetOpen ` ( abs o. - ) ) = ( TopOpen ` CCfld ) )
8 2 4 7 mp2b 
 |-  ( MetOpen ` ( abs o. - ) ) = ( TopOpen ` CCfld )
9 1 8 eqtr4i 
 |-  J = ( MetOpen ` ( abs o. - ) )