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	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	slmdbn0	⊢ ( 𝑊 ∈ SLMod → 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		slmdbn0.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		slmdmnd	⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ Mnd )
3	1	mndbn0	⊢ ( 𝑊 ∈ Mnd → 𝐵 ≠ ∅ )
4	2 3	syl	⊢ ( 𝑊 ∈ SLMod → 𝐵 ≠ ∅ )