Metamath Proof Explorer


Theorem wrdl2exs2

Description: A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021)

Ref Expression
Assertion wrdl2exs2 W Word S W = 2 s S t S W = ⟨“ st ”⟩

Proof

Step Hyp Ref Expression
1 1le2 1 2
2 breq2 W = 2 1 W 1 2
3 1 2 mpbiri W = 2 1 W
4 wrdsymb1 W Word S 1 W W 0 S
5 3 4 sylan2 W Word S W = 2 W 0 S
6 lsw W Word S lastS W = W W 1
7 oveq1 W = 2 W 1 = 2 1
8 2m1e1 2 1 = 1
9 7 8 eqtrdi W = 2 W 1 = 1
10 9 fveq2d W = 2 W W 1 = W 1
11 6 10 sylan9eq W Word S W = 2 lastS W = W 1
12 2nn 2
13 lswlgt0cl 2 W Word S W = 2 lastS W S
14 12 13 mpan W Word S W = 2 lastS W S
15 11 14 eqeltrrd W Word S W = 2 W 1 S
16 wrdlen2s2 W Word S W = 2 W = ⟨“ W 0 W 1 ”⟩
17 id s = W 0 s = W 0
18 eqidd s = W 0 t = t
19 17 18 s2eqd s = W 0 ⟨“ st ”⟩ = ⟨“ W 0 t ”⟩
20 19 eqeq2d s = W 0 W = ⟨“ st ”⟩ W = ⟨“ W 0 t ”⟩
21 eqidd t = W 1 W 0 = W 0
22 id t = W 1 t = W 1
23 21 22 s2eqd t = W 1 ⟨“ W 0 t ”⟩ = ⟨“ W 0 W 1 ”⟩
24 23 eqeq2d t = W 1 W = ⟨“ W 0 t ”⟩ W = ⟨“ W 0 W 1 ”⟩
25 20 24 rspc2ev W 0 S W 1 S W = ⟨“ W 0 W 1 ”⟩ s S t S W = ⟨“ st ”⟩
26 5 15 16 25 syl3anc W Word S W = 2 s S t S W = ⟨“ st ”⟩