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) Revise df-cnfld . (Revised by GG, 31-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem cnfldfunALT

Proof