Metamath Proof Explorer

Theorem gg-cnfldex

Description: The field of complex numbers is a set. Alternative proof of cnfldex . This version directly uses df-cnfld , which is discouraged, however it saves all complex numbers axioms and ax-pow . (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by GG, 16-Mar-2025)

Ref Expression
Assertion gg-cnfldex 
|- CCfld e. _V

Proof

Step Hyp Ref Expression
1 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. - ) ) >. } ) )
2 tpex 
 |-  { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } e. _V
3 snex 
 |-  { <. ( *r ` ndx ) , * >. } e. _V
4 2 3 unex 
 |-  ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) e. _V
5 tpex 
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } e. _V
6 snex 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } e. _V
7 5 6 unex 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) e. _V
8 4 7 unex 
 |-  ( ( { <. ( 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. - ) ) >. } ) ) e. _V
9 1 8 eqeltri 
 |-  CCfld e. _V