Metamath Proof Explorer

Theorem lsw0g

Description: The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018)

Ref Expression
Assertion lsw0g 
|- ( lastS ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 wrd0 
 |-  (/) e. Word V
2 hash0 
 |-  ( # ` (/) ) = 0
3 lsw0 
 |-  ( ( (/) e. Word V /\ ( # ` (/) ) = 0 ) -> ( lastS ` (/) ) = (/) )
4 1 2 3 mp2an 
 |-  ( lastS ` (/) ) = (/)