Theorem cnfldfunALT

Description: The field of complex numbers is a function. Alternate proof of cnfldfun not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 11-Nov-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
2		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
3		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
4		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
5		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
6		fvex	$$⊢{\cdot }_{\mathrm{ndx}}\in \mathrm{V}$$
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8		addex	$$⊢+\in \mathrm{V}$$
9		mulex	$$⊢\times \in \mathrm{V}$$
10	4 5 6 7 8 9	funtp	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}\right)\to \mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
11	1 2 3 10	mp3an	$$⊢\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
12		fvex	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\in \mathrm{V}$$
13		cjf	$$⊢*:ℂ⟶ℂ$$
14		fex	$$⊢\left(*:ℂ⟶ℂ\wedge ℂ\in \mathrm{V}\right)\to *\in \mathrm{V}$$
15	13 7 14	mp2an	$$⊢*\in \mathrm{V}$$
16	12 15	funsn	$$⊢\mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
17	11 16	pm3.2i	$$⊢\left(\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
18	7 8 9	dmtpop	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}$$
19	15	dmsnop	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
20	18 19	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
21		starvndxnbasendx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
22	21	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
23		starvndxnplusgndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
24	23	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
25		starvndxnmulrndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
26	25	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
27		disjtpsn	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
28	22 24 26 27	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
29	20 28	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\varnothing$$
30		funun	$$⊢\left(\left(\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\wedge \mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
31	17 29 30	mp2an	$$⊢\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
32		slotsdifplendx	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\right)$$
33	32	simpri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
34		dsndxntsetndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
35	34	necomi	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
36		slotsdifdsndx	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
37	36	simpri	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
38		fvex	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
39		fvex	$$⊢{\le }_{\mathrm{ndx}}\in \mathrm{V}$$
40		fvex	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
41		fvex	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
42		letsr	$$⊢\le \in \mathrm{TosetRel}$$
43	42	elexi	$$⊢\le \in \mathrm{V}$$
44		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
45		fex	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
46	44 7 45	mp2an	$$⊢\mathrm{abs}\in \mathrm{V}$$
47		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
48	7 7	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
49		fex	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\right)\to -\in \mathrm{V}$$
50	47 48 49	mp2an	$$⊢-\in \mathrm{V}$$
51	46 50	coex	$$⊢\mathrm{abs}\circ -\in \mathrm{V}$$
52	38 39 40 41 43 51	funtp	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\to \mathrm{Fun}\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	33 35 37 52	mp3an	$$⊢\mathrm{Fun}\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\}$$
54		fvex	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
55		fvex	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
56	54 55	funsn	$$⊢\mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
57	53 56	pm3.2i	$$⊢\left(\mathrm{Fun}\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 \mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
58	41 43 51	dmtpop	$$⊢\mathrm{dom}\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\}=\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
59	55	dmsnop	$$⊢\mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}$$
60	58 59	ineq12i	$$⊢\mathrm{dom}\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\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}$$
61		slotsdifunifndx	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
62		unifndxntsetndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
63	62	necomi	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
64	63	a1i	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
65	64	anim1i	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
66		3anass	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\leftrightarrow \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
67	65 66	sylibr	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
68	61 67	ax-mp	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
69		disjtpsn	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
70	68 69	ax-mp	$$⊢\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
71	60 70	eqtri	$$⊢\mathrm{dom}\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\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing$$
72		funun	$$⊢\left(\left(\mathrm{Fun}\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 \mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)\wedge \mathrm{dom}\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\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing \right)\to \mathrm{Fun}\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)$$
73	57 71 72	mp2an	$$⊢\mathrm{Fun}\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)$$
74	31 73	pm3.2i	$$⊢\left(\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{Fun}\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)$$
75		dmun	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
76		dmun	$$⊢\mathrm{dom}\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)=\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
77	75 76	ineq12i	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\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)=\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)$$
78	18 58	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\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\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
79		tsetndxnbasendx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
80	79	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
81		tsetndxnplusgndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
82	81	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
83		tsetndxnmulrndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
84	83	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
85	80 82 84	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\right)$$
86		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
87	86	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
88		plendxnplusgndx	$$⊢{\le }_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
89	88	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
90		plendxnmulrndx	$$⊢{\le }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
91	90	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
92	87 89 91	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\right)$$
93		dsndxnbasendx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
94	93	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
95		dsndxnplusgndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
96	95	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
97		dsndxnmulrndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
98	97	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
99	94 96 98	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
100		disjtp2	$$⊢\left(\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
101	85 92 99 100	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
102	78 101	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\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\}=\varnothing$$
103	18 59	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}$$
104		unifndxnbasendx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
105	104	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
106	105	a1i	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
107		3simpa	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
108		3anass	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\leftrightarrow \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
109	106 107 108	sylanbrc	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
110	109	adantr	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
111	61 110	ax-mp	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
112		disjtpsn	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
113	111 112	ax-mp	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
114	103 113	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing$$
115	102 114	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\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\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing \right)$$
116		undisj2	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\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\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing \right)\leftrightarrow \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
117	115 116	mpbi	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
118	19 58	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\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\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
119		tsetndxnstarvndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
120		necom	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\leftrightarrow {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
121	120	biimpi	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\to {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
122	121	adantr	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\right)\to {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
123	32 122	ax-mp	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
124		necom	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\leftrightarrow \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
125	124	biimpi	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\to \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
126	125	adantr	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\to \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
127	36 126	ax-mp	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
128		disjtpsn	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\right)\to \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
129	119 123 127 128	mp3an	$$⊢\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
130	129	ineqcomi	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
131	118 130	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\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\}=\varnothing$$
132	19 59	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}$$
133		simpl3	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
134	61 133	ax-mp	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
135		disjsn2	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\to \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
136	134 135	ax-mp	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
137	132 136	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing$$
138	131 137	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\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\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing \right)$$
139		undisj2	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\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\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}=\varnothing \right)\leftrightarrow \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
140	138 139	mpbi	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
141	117 140	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing \right)$$
142		undisj1	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing \right)\leftrightarrow \left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
143	141 142	mpbi	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\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 \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}\right)=\varnothing$$
144	77 143	eqtri	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\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)=\varnothing$$
145		funun	$$⊢\left(\left(\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{Fun}\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)\wedge \mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\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)=\varnothing \right)\to \mathrm{Fun}\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)$$
146	74 144 145	mp2an	$$⊢\mathrm{Fun}\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)$$
147		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)$$
148	147	funeqi	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}\leftrightarrow \mathrm{Fun}\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)$$
149	146 148	mpbir	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$