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 = ( Base ` W ) |
|
| Assertion | slmdbn0 | |- ( W e. SLMod -> B =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | slmdbn0.b | |- B = ( Base ` W ) |
|
| 2 | slmdmnd | |- ( W e. SLMod -> W e. Mnd ) |
|
| 3 | 1 | mndbn0 | |- ( W e. Mnd -> B =/= (/) ) |
| 4 | 2 3 | syl | |- ( W e. SLMod -> B =/= (/) ) |