Theorem degenmgmbas

Description: The base set of a degenerate magma. (Contributed by AV, 21-Aug-2026)

	Ref	Expression
Hypotheses	degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
	degenmgmbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	degenmgmbas	⊢ 𝐵 = { ∅ , 1o }

Proof

Step	Hyp	Ref	Expression
1		degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
2		degenmgmbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		prex	⊢ { ∅ , 1o } ∈ V
4	1	grpbase	⊢ ( { ∅ , 1o } ∈ V → { ∅ , 1o } = ( Base ‘ 𝑀 ) )
5	3 4	ax-mp	⊢ { ∅ , 1o } = ( Base ‘ 𝑀 )
6	2 5	eqtr4i	⊢ 𝐵 = { ∅ , 1o }