Metamath Proof Explorer

Theorem cnfldunif

Description: The uniform structure component of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldunif 
|- ( metUnif ` ( abs o. - ) ) = ( UnifSet ` CCfld )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( metUnif ` ( abs o. - ) ) e. _V
2 cnfldstr 
 |-  CCfld Struct <. 1 , ; 1 3 >.
3 unifid 
 |-  UnifSet = Slot ( UnifSet ` ndx )
4 ssun2 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } C_ ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } )
5 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. - ) ) >. } ) )
6 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. - ) ) >. } ) )
7 5 6 sseqtrri 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) C_ CCfld
8 4 7 sstri 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } C_ CCfld
9 2 3 8 strfv 
 |-  ( ( metUnif ` ( abs o. - ) ) e. _V -> ( metUnif ` ( abs o. - ) ) = ( UnifSet ` CCfld ) )
10 1 9 ax-mp 
 |-  ( metUnif ` ( abs o. - ) ) = ( UnifSet ` CCfld )