Theorem slmdbn0

Description: The base set of a semimodule is nonempty. (Contributed by Thierry Arnoux, 1-Apr-2018) (Proof shortened by AV, 10-Jan-2023)

	Ref	Expression
Hypothesis	slmdbn0.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	slmdbn0	$$⊢W\in \mathrm{SLMod}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		slmdbn0.b	$$⊢B={\mathrm{Base}}_W$$
2		slmdmnd	$$⊢W\in \mathrm{SLMod}\to W\in \mathrm{Mnd}$$
3	1	mndbn0	$$⊢W\in \mathrm{Mnd}\to B\ne \varnothing$$
4	2 3	syl	$$⊢W\in \mathrm{SLMod}\to B\ne \varnothing$$