Theorem gg-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) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

	Ref	Expression
Assertion	gg-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}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}$$
5		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
6		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\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		gg-dfcnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\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}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
9	5 8	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\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}}}$$