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 =Basefld

Proof

Step Hyp Ref Expression
1 cnex V
2 cnfldstr fldStruct113
3 baseid Base=SlotBasendx
4 snsstp1 BasendxBasendx+ndx+ndx×
5 ssun1 Basendx+ndx+ndx×Basendx+ndx+ndx×*ndx*
6 ssun1 Basendx+ndx+ndx×*ndx*Basendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
7 df-cnfld fld=Basendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
8 6 7 sseqtrri Basendx+ndx+ndx×*ndx*fld
9 5 8 sstri Basendx+ndx+ndx×fld
10 4 9 sstri Basendxfld
11 2 3 10 strfv V=Basefld
12 1 11 ax-mp =Basefld