Theorem degenmgm

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set ( ( (/) ( +gM ) 1o ) and ( (/) ( +gM ) (/) ) are not defined, and therefore are (/) by definition, which is contained in the base set), and its domain is not (a subset of) the base set ( 2o is in the domain of the operation, but not in the base set) , the structure M is still a magma according to our definition. (Contributed by AV, 18-Aug-2026)

	Ref	Expression
Hypothesis	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\}$$
Assertion	degenmgm	$$⊢M\in \mathrm{Mgm}$$

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		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
4	3 3	pm3.2i	$$⊢\left(\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\wedge \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
5		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
6	5 5	pm3.2i	$$⊢\left(1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\wedge 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
7	4 6	pm3.2i	$$⊢\left(\left(\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\wedge \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)\wedge \left(1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\wedge 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)\right)$$
8		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
9		oveq1	$$⊢x=\varnothing \to x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=\varnothing \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y$$
10		df-ov	$$⊢\varnothing \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)$$
11	9 10	eqtrdi	$$⊢x=\varnothing \to x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)$$
12	11	eleq1d	$$⊢x=\varnothing \to \left(x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
13	12	ralbidv	$$⊢x=\varnothing \to \left(\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
14		oveq1	$$⊢x=1_{𝑜}\to x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=1_{𝑜}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y$$
15		df-ov	$$⊢1_{𝑜}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)$$
16	14 15	eqtrdi	$$⊢x=1_{𝑜}\to x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)$$
17	16	eleq1d	$$⊢x=1_{𝑜}\to \left(x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
18	17	ralbidv	$$⊢x=1_{𝑜}\to \left(\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
19	2 8 13 18	ralpr	$$⊢\forall x\in \left\{\varnothing ,1_{𝑜}\right\}\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\wedge \forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
20		opeq2	$$⊢y=\varnothing \to ⟨\varnothing ,y⟩=⟨\varnothing ,\varnothing ⟩$$
21	20	fveq2d	$$⊢y=\varnothing \to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,\varnothing ⟩\right)$$
22		1n0	$$⊢1_{𝑜}\ne \varnothing$$
23	22	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
24	23	orci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne 1_{𝑜}\right)$$
25	2 2	opthne	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},1_{𝑜}⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne 1_{𝑜}\right)$$
26	24 25	mpbir	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},1_{𝑜}⟩$$
27	23	orci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne 2_{𝑜}\right)$$
28	2 2	opthne	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne 2_{𝑜}\right)$$
29	27 28	mpbir	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},2_{𝑜}⟩$$
30	23	orci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne \varnothing \right)$$
31	2 2	opthne	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},\varnothing ⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee \varnothing \ne \varnothing \right)$$
32	30 31	mpbir	$$⊢⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},\varnothing ⟩$$
33		opex	$$⊢⟨\varnothing ,\varnothing ⟩\in \mathrm{V}$$
34	8 8 8 33	fvtp0	$$⊢\left(⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},1_{𝑜}⟩\wedge ⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\wedge ⟨\varnothing ,\varnothing ⟩\ne ⟨1_{𝑜},\varnothing ⟩\right)\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,\varnothing ⟩\right)=\varnothing$$
35	26 29 32 34	mp3an	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,\varnothing ⟩\right)=\varnothing$$
36	21 35	eqtrdi	$$⊢y=\varnothing \to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)=\varnothing$$
37	36	eleq1d	$$⊢y=\varnothing \to \left(\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
38		opeq2	$$⊢y=1_{𝑜}\to ⟨\varnothing ,y⟩=⟨\varnothing ,1_{𝑜}⟩$$
39	38	fveq2d	$$⊢y=1_{𝑜}\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,1_{𝑜}⟩\right)$$
40	23	orci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne 1_{𝑜}\right)$$
41	2 8	opthne	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},1_{𝑜}⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne 1_{𝑜}\right)$$
42	40 41	mpbir	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},1_{𝑜}⟩$$
43	23	orci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne 2_{𝑜}\right)$$
44	2 8	opthne	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne 2_{𝑜}\right)$$
45	43 44	mpbir	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩$$
46	22	olci	$$⊢\left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne \varnothing \right)$$
47	2 8	opthne	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\leftrightarrow \left(\varnothing \ne 1_{𝑜}\vee 1_{𝑜}\ne \varnothing \right)$$
48	46 47	mpbir	$$⊢⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩$$
49		opex	$$⊢⟨\varnothing ,1_{𝑜}⟩\in \mathrm{V}$$
50	8 8 8 49	fvtp0	$$⊢\left(⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},1_{𝑜}⟩\wedge ⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\wedge ⟨\varnothing ,1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\right)\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,1_{𝑜}⟩\right)=\varnothing$$
51	42 45 48 50	mp3an	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,1_{𝑜}⟩\right)=\varnothing$$
52	39 51	eqtrdi	$$⊢y=1_{𝑜}\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)=\varnothing$$
53	52	eleq1d	$$⊢y=1_{𝑜}\to \left(\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
54	2 8 37 53	ralpr	$$⊢\forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\wedge \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
55		opeq2	$$⊢y=\varnothing \to ⟨1_{𝑜},y⟩=⟨1_{𝑜},\varnothing ⟩$$
56	55	fveq2d	$$⊢y=\varnothing \to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},\varnothing ⟩\right)$$
57	22	olci	$$⊢\left(1_{𝑜}\ne 1_{𝑜}\vee 1_{𝑜}\ne \varnothing \right)$$
58	8 8	opthne	$$⊢⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\leftrightarrow \left(1_{𝑜}\ne 1_{𝑜}\vee 1_{𝑜}\ne \varnothing \right)$$
59	57 58	mpbir	$$⊢⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩$$
60		2on0	$$⊢2_{𝑜}\ne \varnothing$$
61	60	olci	$$⊢\left(1_{𝑜}\ne 1_{𝑜}\vee 2_{𝑜}\ne \varnothing \right)$$
62		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
63	8 62	opthne	$$⊢⟨1_{𝑜},2_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\leftrightarrow \left(1_{𝑜}\ne 1_{𝑜}\vee 2_{𝑜}\ne \varnothing \right)$$
64	61 63	mpbir	$$⊢⟨1_{𝑜},2_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩$$
65		opex	$$⊢⟨1_{𝑜},\varnothing ⟩\in \mathrm{V}$$
66	65 8	fvtp3	$$⊢\left(⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\wedge ⟨1_{𝑜},2_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\right)\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},\varnothing ⟩\right)=1_{𝑜}$$
67	59 64 66	mp2an	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},\varnothing ⟩\right)=1_{𝑜}$$
68	56 67	eqtrdi	$$⊢y=\varnothing \to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)=1_{𝑜}$$
69	68	eleq1d	$$⊢y=\varnothing \to \left(\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
70		opeq2	$$⊢y=1_{𝑜}\to ⟨1_{𝑜},y⟩=⟨1_{𝑜},1_{𝑜}⟩$$
71	70	fveq2d	$$⊢y=1_{𝑜}\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},1_{𝑜}⟩\right)$$
72		1one2o	$$⊢1_{𝑜}\ne 2_{𝑜}$$
73	72	olci	$$⊢\left(1_{𝑜}\ne 1_{𝑜}\vee 1_{𝑜}\ne 2_{𝑜}\right)$$
74	8 8	opthne	$$⊢⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\leftrightarrow \left(1_{𝑜}\ne 1_{𝑜}\vee 1_{𝑜}\ne 2_{𝑜}\right)$$
75	73 74	mpbir	$$⊢⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩$$
76		opex	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \mathrm{V}$$
77	76 8	fvtp1	$$⊢\left(⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},2_{𝑜}⟩\wedge ⟨1_{𝑜},1_{𝑜}⟩\ne ⟨1_{𝑜},\varnothing ⟩\right)\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},1_{𝑜}⟩\right)=1_{𝑜}$$
78	75 59 77	mp2an	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},1_{𝑜}⟩\right)=1_{𝑜}$$
79	71 78	eqtrdi	$$⊢y=1_{𝑜}\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)=1_{𝑜}$$
80	79	eleq1d	$$⊢y=1_{𝑜}\to \left(\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
81	2 8 69 80	ralpr	$$⊢\forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\wedge 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
82	54 81	anbi12i	$$⊢\left(\forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨\varnothing ,y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\wedge \forall y\in \left\{\varnothing ,1_{𝑜}\right\}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\left(⟨1_{𝑜},y⟩\right)\in \left\{\varnothing ,1_{𝑜}\right\}\right)\leftrightarrow \left(\left(\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\wedge \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)\wedge \left(1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\wedge 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)\right)$$
83	19 82	bitri	$$⊢\forall x\in \left\{\varnothing ,1_{𝑜}\right\}\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\leftrightarrow \left(\left(\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\wedge \varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\right)\wedge \left(1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\wedge 1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}\right)\right)$$
84	7 83	mpbir	$$⊢\forall x\in \left\{\varnothing ,1_{𝑜}\right\}\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}$$
85		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
86	1 85	degenmgmbas	$$⊢{\mathrm{Base}}_M=\left\{\varnothing ,1_{𝑜}\right\}$$
87	86	eqcomi	$$⊢\left\{\varnothing ,1_{𝑜}\right\}={\mathrm{Base}}_M$$
88		tpex	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\in \mathrm{V}$$
89	1	grpplusg	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\in \mathrm{V}\to \left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}={+}_M$$
90	88 89	ax-mp	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}={+}_M$$
91	87 90	ismgmn0	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in \left\{\varnothing ,1_{𝑜}\right\}\forall y\in \left\{\varnothing ,1_{𝑜}\right\}x\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}y\in \left\{\varnothing ,1_{𝑜}\right\}\right)$$
92	84 91	mpbiri	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}\to M\in \mathrm{Mgm}$$
93	3 92	ax-mp	$$⊢M\in \mathrm{Mgm}$$