Metamath Proof Explorer


Theorem wrdlndm

Description: The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021) (Proof shortened by JJ, 18-Nov-2022)

Ref Expression
Assertion wrdlndm WWordVWdomW

Proof

Step Hyp Ref Expression
1 fzonel ¬W0..^W
2 1 a1i WWordV¬W0..^W
3 wrddm WWordVdomW=0..^W
4 2 3 neleqtrrd WWordV¬WdomW
5 df-nel WdomW¬WdomW
6 4 5 sylibr WWordVWdomW