Metamath Proof Explorer

Theorem wrdlen3s3

Description: A word of length three as length 3 string. (Contributed by AV, 26-Jan-2021)

Ref Expression
Assertion wrdlen3s3 ⊢W∈WordV∧W=3→W=⟨“W⁡0W⁡1W⁡2”⟩

Proof

Step Hyp Ref Expression
1 wrd3tpop ⊢W∈WordV∧W=3→W=0W⁡01W⁡12W⁡2
2 fvex ⊢W⁡0∈V
3 fvex ⊢W⁡1∈V
4 fvex ⊢W⁡2∈V
5 s3tpop ⊢W⁡0∈V∧W⁡1∈V∧W⁡2∈V→⟨“W⁡0W⁡1W⁡2”⟩=0W⁡01W⁡12W⁡2
6 5 eqcomd ⊢W⁡0∈V∧W⁡1∈V∧W⁡2∈V→0W⁡01W⁡12W⁡2=⟨“W⁡0W⁡1W⁡2”⟩
7 2 3 4 6 mp3an ⊢0W⁡01W⁡12W⁡2=⟨“W⁡0W⁡1W⁡2”⟩
8 1 7 eqtrdi ⊢W∈WordV∧W=3→W=⟨“W⁡0W⁡1W⁡2”⟩