Theorem degenmgm2opdm

Description: The domain of the operation of a second degenerate magma. (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	degenmgm2opdm	$$⊢\mathrm{dom}{+}_M=\left\{1_{𝑜}\right\}\times \left\{1_{𝑜},2_{𝑜}\right\}$$

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		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
3		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
4	2 2 3	dmtpop	$$⊢\mathrm{dom}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
5		tpex	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}\in \mathrm{V}$$
6	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$$
7	5 6	ax-mp	$$⊢\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}={+}_M$$
8	7	eqcomi	$$⊢{+}_M=\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}$$
9	8	dmeqi	$$⊢\mathrm{dom}{+}_M=\mathrm{dom}\left\{⟨⟨1_{𝑜},1_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,1_{𝑜}⟩,⟨⟨1_{𝑜},2_{𝑜}⟩,2_{𝑜}⟩\right\}$$
10		xpsnprg	$$⊢\left(1_{𝑜}\in \mathrm{V}\wedge 1_{𝑜}\in \mathrm{V}\wedge 2_{𝑜}\in \mathrm{V}\right)\to \left\{1_{𝑜}\right\}\times \left\{1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
11	2 2 3 10	mp3an	$$⊢\left\{1_{𝑜}\right\}\times \left\{1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
12		tpidm23	$$⊢\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
13	11 12	eqtr4i	$$⊢\left\{1_{𝑜}\right\}\times \left\{1_{𝑜},2_{𝑜}\right\}=\left\{⟨1_{𝑜},1_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨1_{𝑜},2_{𝑜}⟩\right\}$$
14	4 9 13	3eqtr4i	$$⊢\mathrm{dom}{+}_M=\left\{1_{𝑜}\right\}\times \left\{1_{𝑜},2_{𝑜}\right\}$$