Theorem mndbn0

Description: The base set of a monoid is not empty. Statement in Lang p. 3. (Contributed by AV, 29-Dec-2023)

	Ref	Expression
Hypothesis	mndbn0.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	mndbn0	$$⊢G\in \mathrm{Mnd}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		mndbn0.b	$$⊢B={\mathrm{Base}}_G$$
2		eqid	$$⊢0_G=0_G$$
3	1 2	mndidcl	$$⊢G\in \mathrm{Mnd}\to 0_G\in B$$
4	3	ne0d	$$⊢G\in \mathrm{Mnd}\to B\ne \varnothing$$