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 ⊢W∈WordV→W∉dom⁡W

Proof

Step Hyp Ref Expression
1 fzonel ⊢¬W∈0..^W
2 1 a1i ⊢W∈WordV→¬W∈0..^W
3 wrddm ⊢W∈WordV→dom⁡W=0..^W
4 2 3 neleqtrrd ⊢W∈WordV→¬W∈dom⁡W
5 df-nel ⊢W∉dom⁡W↔¬W∈dom⁡W
6 4 5 sylibr ⊢W∈WordV→W∉dom⁡W