Theorem degenmgmbas

Description: The base set of a degenerate magma. (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	degenmgmbas	$$⊢B=\left\{\varnothing ,1_{𝑜}\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		prex	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}$$
4	1	grpbase	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\in \mathrm{V}\to \left\{\varnothing ,1_{𝑜}\right\}={\mathrm{Base}}_M$$
5	3 4	ax-mp	$$⊢\left\{\varnothing ,1_{𝑜}\right\}={\mathrm{Base}}_M$$
6	2 5	eqtr4i	$$⊢B=\left\{\varnothing ,1_{𝑜}\right\}$$