Theorem degenmgmnfn

Description: The operation of a degenerate magma is not a function on its base set. (Contributed by AV, 21-Aug-2026)

	Ref	Expression
Hypotheses	degenmgm.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{\varnothing ,1_{𝑜}\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}⟩\right\}$$
	degenmgmbas.b	$$⊢B={\mathrm{Base}}_M$$
Assertion	degenmgmnfn	$$⊢\neg {+}_{M}Fn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		degenmgm.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{\varnothing ,1_{𝑜}\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}⟩\right\}$$
2		degenmgmbas.b	$$⊢B={\mathrm{Base}}_M$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
5		1n0	$$⊢1_{𝑜}\ne \varnothing$$
6	5	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
7		prnesn	$$⊢\left(\varnothing \in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{V}\wedge \varnothing \ne 1_{𝑜}\right)\to \left\{\varnothing ,1_{𝑜}\right\}\ne \left\{1_{𝑜}\right\}$$
8	3 4 6 7	mp3an	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\ne \left\{1_{𝑜}\right\}$$
9	8	nesymi	$$⊢\neg \left\{1_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}$$
10	9	intnanr	$$⊢\neg \left(\left\{1_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\wedge \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)$$
11	4	snnz	$$⊢\left\{1_{𝑜}\right\}\ne \varnothing$$
12	3	tpnz	$$⊢\left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\ne \varnothing$$
13		xp11	$$⊢\left(\left\{1_{𝑜}\right\}\ne \varnothing \wedge \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}\ne \varnothing \right)\to \left(\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\left\{1_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\wedge \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)\right)$$
14	11 12 13	mp2an	$$⊢\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\left\{1_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\wedge \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\right)$$
15	10 14	mtbir	$$⊢\neg \left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜}\right\}$$
16	1	degenmgmopdm	$$⊢\mathrm{dom}{+}_M=\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$
17	1 2	degenmgmbas	$$⊢B=\left\{\varnothing ,1_{𝑜}\right\}$$
18	17 17	xpeq12i	$$⊢B\times B=\left\{\varnothing ,1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜}\right\}$$
19	16 18	eqeq12i	$$⊢\mathrm{dom}{+}_M=B\times B\leftrightarrow \left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{\varnothing ,1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜}\right\}$$
20	15 19	mtbir	$$⊢\neg \mathrm{dom}{+}_M=B\times B$$
21	20	intnan	$$⊢\neg \left(\mathrm{Fun}{+}_M\wedge \mathrm{dom}{+}_M=B\times B\right)$$
22		df-fn	$$⊢{+}_{M}Fn\left(B\times B\right)\leftrightarrow \left(\mathrm{Fun}{+}_M\wedge \mathrm{dom}{+}_M=B\times B\right)$$
23	21 22	mtbir	$$⊢\neg {+}_{M}Fn\left(B\times B\right)$$