Metamath Proof Explorer


Theorem wrdlen1

Description: A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018) (Proof shortened by AV, 19-Oct-2018)

Ref Expression
Assertion wrdlen1 WWordVW=1vVW0=v

Proof

Step Hyp Ref Expression
1 1le1 11
2 breq2 W=11W11
3 1 2 mpbiri W=11W
4 wrdsymb1 WWordV1WW0V
5 3 4 sylan2 WWordVW=1W0V
6 clel5 W0VvVW0=v
7 5 6 sylib WWordVW=1vVW0=v