# 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 ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 cnfldstr ${⊢}{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$
3 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
4 snsstp1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}$
5 ssun1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}$
6 ssun1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$
7 df-cnfld ${⊢}{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$
8 6 7 sseqtrri ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$
9 5 8 sstri ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$
10 4 9 sstri ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$
11 2 3 10 strfv ${⊢}ℂ\in \mathrm{V}\to ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
12 1 11 ax-mp ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$