Theorem degenmgmopdm

Description: The domain of the operation of a degenerate magma. (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	degenmgmopdm	$$⊢\mathrm{dom}{+}_M=\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\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		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
3	2 2 2	dmtpop	$$⊢\mathrm{dom}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},\varnothing ⟩\right\}$$
4		tpex	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}\in \mathrm{V}$$
5	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$$
6	4 5	ax-mp	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}={+}_M$$
7	6	eqcomi	$$⊢{+}_M=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}$$
8	7	dmeqi	$$⊢\mathrm{dom}{+}_M=\mathrm{dom}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},\varnothing ⟩,1_{𝑜}⟩\right\}$$
9		0ex	$$⊢\varnothing \in \mathrm{V}$$
10		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
11		xpsntpg	$$⊢\left(\left(1_{𝑜}\in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\wedge \left(1_{𝑜}\in \mathrm{V}\wedge 2_{𝑜}\in \mathrm{V}\right)\right)\to \left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
12	2 9 2 10 11	mp4an	$$⊢\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
13		tprot	$$⊢\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},\varnothing ⟩\right\}$$
14	12 13	eqtri	$$⊢\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},\varnothing ⟩\right\}$$
15	3 8 14	3eqtr4i	$$⊢\mathrm{dom}{+}_M=\left\{1_{𝑜}\right\}\times \left\{\varnothing ,1_{𝑜},2_{𝑜}\right\}$$