Theorem degenmgm2

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set, and its domain is not (a subset of) the base set, and the operation is not a function (see degenmgm2nfun ), the structure M is still a magma according to our definition. (Contributed by AV, 21-Aug-2026)

	Ref	Expression
Hypothesis	degenmgm2.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{\varnothing ,1_{𝑜}\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}⟩\right\}$$
Assertion	degenmgm2	$$⊢M\in \mathrm{Mgm}$$

Proof

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