Theorem cnfldfun

Description: The field of complex numbers is a function. (Contributed by AV, 14-Nov-2021)

	Ref	Expression
Assertion	cnfldfun	$$⊢\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		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
22		1re	$$⊢1\in ℝ$$
23		1lt4	$$⊢1<4$$
24	22 23	ltneii	$$⊢1\ne 4$$
25		starvndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}=4$$
26	24 25	neeqtrri	$$⊢1\ne {\mathrm{*}}_{\mathrm{ndx}}$$
27	21 26	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
28		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
29		2re	$$⊢2\in ℝ$$
30		2lt4	$$⊢2<4$$
31	29 30	ltneii	$$⊢2\ne 4$$
32	31 25	neeqtrri	$$⊢2\ne {\mathrm{*}}_{\mathrm{ndx}}$$
33	28 32	eqnetri	$$⊢{+}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
34		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
35		3re	$$⊢3\in ℝ$$
36		3lt4	$$⊢3<4$$
37	35 36	ltneii	$$⊢3\ne 4$$
38	37 25	neeqtrri	$$⊢3\ne {\mathrm{*}}_{\mathrm{ndx}}$$
39	34 38	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
40		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$$
41	27 33 39 40	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
42	20 41	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\varnothing$$
43		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)$$
44	17 42 43	mp2an	$$⊢\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
45		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
46		9re	$$⊢9\in ℝ$$
47		9lt10	$$⊢9<10$$
48	46 47	ltneii	$$⊢9\ne 10$$
49		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
50	48 49	neeqtrri	$$⊢9\ne {\le }_{\mathrm{ndx}}$$
51	45 50	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
52		1nn	$$⊢1\in \mathbb{N}$$
53		2nn0	$$⊢2\in {\mathbb{N}}_0$$
54		9nn0	$$⊢9\in {\mathbb{N}}_0$$
55	46	leidi	$$⊢9\le 9$$
56	52 53 54 55	decltdi	$$⊢9<12$$
57	46 56	ltneii	$$⊢9\ne 12$$
58		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
59	57 58	neeqtrri	$$⊢9\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
60	45 59	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
61		10re	$$⊢10\in ℝ$$
62		1nn0	$$⊢1\in {\mathbb{N}}_0$$
63		0nn0	$$⊢0\in {\mathbb{N}}_0$$
64		2nn	$$⊢2\in \mathbb{N}$$
65		2pos	$$⊢0<2$$
66	62 63 64 65	declt	$$⊢10<12$$
67	61 66	ltneii	$$⊢10\ne 12$$
68	67 58	neeqtrri	$$⊢10\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
69	49 68	eqnetri	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
70		fvex	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
71		fvex	$$⊢{\le }_{\mathrm{ndx}}\in \mathrm{V}$$
72		fvex	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
73		fvex	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
74		letsr	$$⊢\le \in \mathrm{TosetRel}$$
75	74	elexi	$$⊢\le \in \mathrm{V}$$
76		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
77		fex	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
78	76 7 77	mp2an	$$⊢\mathrm{abs}\in \mathrm{V}$$
79		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
80	7 7	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
81		fex	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\right)\to -\in \mathrm{V}$$
82	79 80 81	mp2an	$$⊢-\in \mathrm{V}$$
83	78 82	coex	$$⊢\mathrm{abs}\circ -\in \mathrm{V}$$
84	70 71 72 73 75 83	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\}$$
85	51 60 69 84	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\}$$
86		fvex	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
87		fvex	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
88	86 87	funsn	$$⊢\mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩\right\}$$
89	85 88	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)$$
90	73 75 83	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\}$$
91	87	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\}$$
92	90 91	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\}$$
93		3nn0	$$⊢3\in {\mathbb{N}}_0$$
94	52 93 54 55	decltdi	$$⊢9<13$$
95	46 94	ltneii	$$⊢9\ne 13$$
96		unifndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)=13$$
97	95 96	neeqtrri	$$⊢9\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
98	45 97	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
99		3nn	$$⊢3\in \mathbb{N}$$
100		3pos	$$⊢0<3$$
101	62 63 99 100	declt	$$⊢10<13$$
102	61 101	ltneii	$$⊢10\ne 13$$
103	102 96	neeqtrri	$$⊢10\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
104	49 103	eqnetri	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
105	62 53	deccl	$$⊢12\in {\mathbb{N}}_0$$
106	105	nn0rei	$$⊢12\in ℝ$$
107		2lt3	$$⊢2<3$$
108	62 53 99 107	declt	$$⊢12<13$$
109	106 108	ltneii	$$⊢12\ne 13$$
110	109 96	neeqtrri	$$⊢12\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
111	58 110	eqnetri	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
112		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$$
113	98 104 111 112	mp3an	$$⊢\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$$
114	92 113	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$$
115		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)$$
116	89 114 115	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)$$
117	44 116	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)$$
118		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\}$$
119		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\}$$
120	118 119	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)$$
121	18 90	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\}$$
122		1lt9	$$⊢1<9$$
123	22 122	ltneii	$$⊢1\ne 9$$
124	123 45	neeqtrri	$$⊢1\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
125	21 124	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
126		2lt9	$$⊢2<9$$
127	29 126	ltneii	$$⊢2\ne 9$$
128	127 45	neeqtrri	$$⊢2\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
129	28 128	eqnetri	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
130		3lt9	$$⊢3<9$$
131	35 130	ltneii	$$⊢3\ne 9$$
132	131 45	neeqtrri	$$⊢3\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
133	34 132	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
134	125 129 133	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)$$
135		1lt10	$$⊢1<10$$
136	22 135	ltneii	$$⊢1\ne 10$$
137	136 49	neeqtrri	$$⊢1\ne {\le }_{\mathrm{ndx}}$$
138	21 137	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
139		2lt10	$$⊢2<10$$
140	29 139	ltneii	$$⊢2\ne 10$$
141	140 49	neeqtrri	$$⊢2\ne {\le }_{\mathrm{ndx}}$$
142	28 141	eqnetri	$$⊢{+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
143		3lt10	$$⊢3<10$$
144	35 143	ltneii	$$⊢3\ne 10$$
145	144 49	neeqtrri	$$⊢3\ne {\le }_{\mathrm{ndx}}$$
146	34 145	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
147	138 142 146	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)$$
148	22 46 122	ltleii	$$⊢1\le 9$$
149	52 53 62 148	decltdi	$$⊢1<12$$
150	22 149	ltneii	$$⊢1\ne 12$$
151	150 58	neeqtrri	$$⊢1\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
152	21 151	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
153	29 46 126	ltleii	$$⊢2\le 9$$
154	52 53 53 153	decltdi	$$⊢2<12$$
155	29 154	ltneii	$$⊢2\ne 12$$
156	155 58	neeqtrri	$$⊢2\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
157	28 156	eqnetri	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
158	35 46 130	ltleii	$$⊢3\le 9$$
159	52 53 93 158	decltdi	$$⊢3<12$$
160	35 159	ltneii	$$⊢3\ne 12$$
161	160 58	neeqtrri	$$⊢3\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
162	34 161	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
163	152 157 162	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)$$
164		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$$
165	134 147 163 164	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$$
166	121 165	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$$
167	18 91	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\}$$
168	52 93 62 148	decltdi	$$⊢1<13$$
169	22 168	ltneii	$$⊢1\ne 13$$
170	169 96	neeqtrri	$$⊢1\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
171	21 170	eqnetri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
172	52 93 53 153	decltdi	$$⊢2<13$$
173	29 172	ltneii	$$⊢2\ne 13$$
174	173 96	neeqtrri	$$⊢2\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
175	28 174	eqnetri	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
176	52 93 93 158	decltdi	$$⊢3<13$$
177	35 176	ltneii	$$⊢3\ne 13$$
178	177 96	neeqtrri	$$⊢3\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
179	34 178	eqnetri	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
180		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$$
181	171 175 179 180	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
182	167 181	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$$
183	166 182	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)$$
184		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$$
185	183 184	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$$
186	19 90	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\}$$
187		incom	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
188		4re	$$⊢4\in ℝ$$
189		4lt9	$$⊢4<9$$
190	188 189	gtneii	$$⊢9\ne 4$$
191	190 25	neeqtrri	$$⊢9\ne {\mathrm{*}}_{\mathrm{ndx}}$$
192	45 191	eqnetri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
193		4lt10	$$⊢4<10$$
194	188 193	gtneii	$$⊢10\ne 4$$
195	194 25	neeqtrri	$$⊢10\ne {\mathrm{*}}_{\mathrm{ndx}}$$
196	49 195	eqnetri	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
197		4nn0	$$⊢4\in {\mathbb{N}}_0$$
198	188 46 189	ltleii	$$⊢4\le 9$$
199	52 53 197 198	decltdi	$$⊢4<12$$
200	188 199	gtneii	$$⊢12\ne 4$$
201	200 25	neeqtrri	$$⊢12\ne {\mathrm{*}}_{\mathrm{ndx}}$$
202	58 201	eqnetri	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
203		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$$
204	192 196 202 203	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$$
205	187 204	eqtri	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
206	186 205	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$$
207	19 91	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\}$$
208	52 93 197 198	decltdi	$$⊢4<13$$
209	188 208	ltneii	$$⊢4\ne 13$$
210	209 96	neeqtrri	$$⊢4\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
211	25 210	eqnetri	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
212		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$$
213	211 212	ax-mp	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
214	207 213	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$$
215	206 214	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)$$
216		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$$
217	215 216	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$$
218	185 217	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)$$
219		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$$
220	218 219	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$$
221	120 220	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$$
222		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)$$
223	117 221 222	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)$$
224		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)$$
225	224	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)$$
226	223 225	mpbir	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$