Theorem cnfldex

Description: The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Avoid complex number axioms and ax-pow . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Assertion	cnfldex	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\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)$$
2		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\in \mathrm{V}$$
3		snex	$$⊢\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\in \mathrm{V}$$
4	2 3	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\in \mathrm{V}$$
5		tpex	$$⊢\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\}\in \mathrm{V}$$
6		snex	$$⊢\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\in \mathrm{V}$$
7	5 6	unex	$$⊢\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\}\in \mathrm{V}$$
8	4 7	unex	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\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)\in \mathrm{V}$$
9	1 8	eqeltri	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}$$