Metamath Proof Explorer


Theorem cnfldtset

Description: The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldtset
|- ( MetOpen ` ( abs o. - ) ) = ( TopSet ` CCfld )

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( MetOpen ` ( abs o. - ) ) e. _V
2 cnfldstr
 |-  CCfld Struct <. 1 , ; 1 3 >.
3 tsetid
 |-  TopSet = Slot ( TopSet ` ndx )
4 snsstp1
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. } C_ { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. }
5 ssun1
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } C_ ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
6 ssun2
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
7 df-cnfld
 |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )
8 6 7 sseqtrri
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) C_ CCfld
9 5 8 sstri
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } C_ CCfld
10 4 9 sstri
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. } C_ CCfld
11 2 3 10 strfv
 |-  ( ( MetOpen ` ( abs o. - ) ) e. _V -> ( MetOpen ` ( abs o. - ) ) = ( TopSet ` CCfld ) )
12 1 11 ax-mp
 |-  ( MetOpen ` ( abs o. - ) ) = ( TopSet ` CCfld )