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 ∈ Word V → W ∉ dom ⁡ W

Proof

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