Metamath Proof Explorer


Theorem wrdlen2s2

Description: A word of length two as doubleton word. (Contributed by AV, 20-Oct-2018)

Ref Expression
Assertion wrdlen2s2 W Word V W = 2 W = ⟨“ W 0 W 1 ”⟩

Proof

Step Hyp Ref Expression
1 wrd2pr2op W Word V W = 2 W = 0 W 0 1 W 1
2 fvex W 0 V
3 fvex W 1 V
4 s2prop W 0 V W 1 V ⟨“ W 0 W 1 ”⟩ = 0 W 0 1 W 1
5 4 eqcomd W 0 V W 1 V 0 W 0 1 W 1 = ⟨“ W 0 W 1 ”⟩
6 2 3 5 mp2an 0 W 0 1 W 1 = ⟨“ W 0 W 1 ”⟩
7 1 6 eqtrdi W Word V W = 2 W = ⟨“ W 0 W 1 ”⟩