Theorem cnfldfun

Description: The field of complex numbers is a function. The proof is much shorter than the proof of cnfldfunALT by using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld . (Contributed by AV, 18-Nov-2021)

	Ref	Expression
Assertion	cnfldfun	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$

Proof

Step	Hyp	Ref	Expression
1		cnfldstr	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$$
2		structn0fun	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩\to \mathrm{Fun}\left({ℂ}_{\mathrm{fld}}\setminus \left\{\varnothing \right\}\right)$$
3		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
4		cnex	$$⊢ℂ\in \mathrm{V}$$
5	3 4	opnzi	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\ne \varnothing$$
6	5	nesymi	$$⊢\neg \varnothing =⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩$$
7		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
8		addex	$$⊢+\in \mathrm{V}$$
9	7 8	opnzi	$$⊢⟨{+}_{\mathrm{ndx}},+⟩\ne \varnothing$$
10	9	nesymi	$$⊢\neg \varnothing =⟨{+}_{\mathrm{ndx}},+⟩$$
11		fvex	$$⊢{\cdot }_{\mathrm{ndx}}\in \mathrm{V}$$
12		mulex	$$⊢\times \in \mathrm{V}$$
13	11 12	opnzi	$$⊢⟨{\cdot }_{\mathrm{ndx}},\times ⟩\ne \varnothing$$
14	13	nesymi	$$⊢\neg \varnothing =⟨{\cdot }_{\mathrm{ndx}},\times ⟩$$
15		3ioran	$$⊢\neg \left(\varnothing =⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\vee \varnothing =⟨{+}_{\mathrm{ndx}},+⟩\vee \varnothing =⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right)\leftrightarrow \left(\neg \varnothing =⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\wedge \neg \varnothing =⟨{+}_{\mathrm{ndx}},+⟩\wedge \neg \varnothing =⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right)$$
16		0ex	$$⊢\varnothing \in \mathrm{V}$$
17	16	eltp	$$⊢\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\leftrightarrow \left(\varnothing =⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\vee \varnothing =⟨{+}_{\mathrm{ndx}},+⟩\vee \varnothing =⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right)$$
18	15 17	xchnxbir	$$⊢\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\leftrightarrow \left(\neg \varnothing =⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\wedge \neg \varnothing =⟨{+}_{\mathrm{ndx}},+⟩\wedge \neg \varnothing =⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right)$$
19	6 10 14 18	mpbir3an	$$⊢\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
20		fvex	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\in \mathrm{V}$$
21		cjf	$$⊢*:ℂ⟶ℂ$$
22		fex	$$⊢\left(*:ℂ⟶ℂ\wedge ℂ\in \mathrm{V}\right)\to *\in \mathrm{V}$$
23	21 4 22	mp2an	$$⊢*\in \mathrm{V}$$
24	20 23	opnzi	$$⊢⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\ne \varnothing$$
25	24	necomi	$$⊢\varnothing \ne ⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩$$
26		nelsn	$$⊢\varnothing \ne ⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\to \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
27	25 26	ax-mp	$$⊢\neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
28	19 27	pm3.2i	$$⊢\left(\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
29		fvex	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
30		fvex	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
31	29 30	opnzi	$$⊢⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩\ne \varnothing$$
32	31	nesymi	$$⊢\neg \varnothing =⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩$$
33		fvex	$$⊢{\le }_{\mathrm{ndx}}\in \mathrm{V}$$
34		letsr	$$⊢\le \in \mathrm{TosetRel}$$
35	34	elexi	$$⊢\le \in \mathrm{V}$$
36	33 35	opnzi	$$⊢⟨{\le }_{\mathrm{ndx}},\le ⟩\ne \varnothing$$
37	36	nesymi	$$⊢\neg \varnothing =⟨{\le }_{\mathrm{ndx}},\le ⟩$$
38		fvex	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
39		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
40		fex	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
41	39 4 40	mp2an	$$⊢\mathrm{abs}\in \mathrm{V}$$
42		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
43	4 4	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
44		fex	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\right)\to -\in \mathrm{V}$$
45	42 43 44	mp2an	$$⊢-\in \mathrm{V}$$
46	41 45	coex	$$⊢\mathrm{abs}\circ -\in \mathrm{V}$$
47	38 46	opnzi	$$⊢⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\ne \varnothing$$
48	47	nesymi	$$⊢\neg \varnothing =⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩$$
49		3ioran	$$⊢\neg \left(\varnothing =⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩\vee \varnothing =⟨{\le }_{\mathrm{ndx}},\le ⟩\vee \varnothing =⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right)\leftrightarrow \left(\neg \varnothing =⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩\wedge \neg \varnothing =⟨{\le }_{\mathrm{ndx}},\le ⟩\wedge \neg \varnothing =⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right)$$
50	32 37 48 49	mpbir3an	$$⊢\neg \left(\varnothing =⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩\vee \varnothing =⟨{\le }_{\mathrm{ndx}},\le ⟩\vee \varnothing =⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right)$$
51	16	eltp	$$⊢\varnothing \in \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\}\leftrightarrow \left(\varnothing =⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩\vee \varnothing =⟨{\le }_{\mathrm{ndx}},\le ⟩\vee \varnothing =⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right)$$
52	50 51	mtbir	$$⊢\neg \varnothing \in \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\}$$
53		fvex	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
54		fvex	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
55	53 54	opnzi	$$⊢⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\ne \varnothing$$
56	55	necomi	$$⊢\varnothing \ne ⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩$$
57		nelsn	$$⊢\varnothing \ne ⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\to \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
58	56 57	ax-mp	$$⊢\neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
59	52 58	pm3.2i	$$⊢\left(\neg \varnothing \in \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\}\wedge \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
60	28 59	pm3.2i	$$⊢\left(\left(\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \left(\neg \varnothing \in \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\}\wedge \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
61		ioran	$$⊢\neg \left(\left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)\leftrightarrow \left(\neg \left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \neg \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
62		ioran	$$⊢\neg \left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\leftrightarrow \left(\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
63		ioran	$$⊢\neg \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\leftrightarrow \left(\neg \varnothing \in \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\}\wedge \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
64	62 63	anbi12i	$$⊢\left(\neg \left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \neg \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)\leftrightarrow \left(\left(\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \left(\neg \varnothing \in \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\}\wedge \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
65	61 64	bitri	$$⊢\neg \left(\left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)\leftrightarrow \left(\left(\neg \varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \neg \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \left(\neg \varnothing \in \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\}\wedge \neg \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
66	60 65	mpbir	$$⊢\neg \left(\left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
67		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)$$
68	67	eleq2i	$$⊢\varnothing \in {ℂ}_{\mathrm{fld}}\leftrightarrow \varnothing \in \left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)\right)$$
69		elun	$$⊢\varnothing \in \left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)\right)\leftrightarrow \left(\varnothing \in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \varnothing \in \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)\right)$$
70		elun	$$⊢\varnothing \in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\leftrightarrow \left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
71		elun	$$⊢\varnothing \in \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)\leftrightarrow \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
72	70 71	orbi12i	$$⊢\left(\varnothing \in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \varnothing \in \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)\right)\leftrightarrow \left(\left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
73	68 69 72	3bitri	$$⊢\varnothing \in {ℂ}_{\mathrm{fld}}\leftrightarrow \left(\left(\varnothing \in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee \varnothing \in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee \left(\varnothing \in \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\}\vee \varnothing \in \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\right)$$
74	66 73	mtbir	$$⊢\neg \varnothing \in {ℂ}_{\mathrm{fld}}$$
75		disjsn	$$⊢{ℂ}_{\mathrm{fld}}\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow \neg \varnothing \in {ℂ}_{\mathrm{fld}}$$
76	74 75	mpbir	$$⊢{ℂ}_{\mathrm{fld}}\cap \left\{\varnothing \right\}=\varnothing$$
77		disjdif2	$$⊢{ℂ}_{\mathrm{fld}}\cap \left\{\varnothing \right\}=\varnothing \to {ℂ}_{\mathrm{fld}}\setminus \left\{\varnothing \right\}={ℂ}_{\mathrm{fld}}$$
78	76 77	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\setminus \left\{\varnothing \right\}={ℂ}_{\mathrm{fld}}$$
79	78	funeqi	$$⊢\mathrm{Fun}\left({ℂ}_{\mathrm{fld}}\setminus \left\{\varnothing \right\}\right)\leftrightarrow \mathrm{Fun}{ℂ}_{\mathrm{fld}}$$
80	2 79	sylib	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩\to \mathrm{Fun}{ℂ}_{\mathrm{fld}}$$
81	1 80	ax-mp	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$