Metamath Proof Explorer

Theorem lencl

Description: The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion lencl 
|- ( W e. Word S -> ( # ` W ) e. NN0 )

Proof

Step Hyp Ref Expression
1 wrdfin 
 |-  ( W e. Word S -> W e. Fin )
2 hashcl 
 |-  ( W e. Fin -> ( # ` W ) e. NN0 )
3 1 2 syl 
 |-  ( W e. Word S -> ( # ` W ) e. NN0 )