Metamath Proof Explorer


Theorem cnfldbas

Description: The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion cnfldbas = Base fld

Proof

Step Hyp Ref Expression
1 cnex V
2 cnfldstr fld Struct 1 13
3 baseid Base = Slot Base ndx
4 snsstp1 Base ndx Base ndx + ndx + ndx ×
5 ssun1 Base ndx + ndx + ndx × Base ndx + ndx + ndx × * ndx *
6 ssun1 Base ndx + ndx + ndx × * ndx * Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
7 df-cnfld fld = Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
8 6 7 sseqtrri Base ndx + ndx + ndx × * ndx * fld
9 5 8 sstri Base ndx + ndx + ndx × fld
10 4 9 sstri Base ndx fld
11 2 3 10 strfv V = Base fld
12 1 11 ax-mp = Base fld