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 e. Word V -> ( # ` W ) e/ dom W )

Proof

Step Hyp Ref Expression
1 fzonel
 |-  -. ( # ` W ) e. ( 0 ..^ ( # ` W ) )
2 1 a1i
 |-  ( W e. Word V -> -. ( # ` W ) e. ( 0 ..^ ( # ` W ) ) )
3 wrddm
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
4 2 3 neleqtrrd
 |-  ( W e. Word V -> -. ( # ` W ) e. dom W )
5 df-nel
 |-  ( ( # ` W ) e/ dom W <-> -. ( # ` W ) e. dom W )
6 4 5 sylibr
 |-  ( W e. Word V -> ( # ` W ) e/ dom W )