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 ∈ Word V ∧ W = 3 → W = ⟨“ W ⁡ 0 W ⁡ 1 W ⁡ 2 ”⟩

Proof

Step Hyp Ref Expression
1 wrd3tpop ⊢ W ∈ Word V ∧ W = 3 → W = 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 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 ⁡ 0 W ⁡ 1 W ⁡ 2 ”⟩ = 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2
6 5 eqcomd ⊢ W ⁡ 0 ∈ V ∧ W ⁡ 1 ∈ V ∧ W ⁡ 2 ∈ V → 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2 = ⟨“ W ⁡ 0 W ⁡ 1 W ⁡ 2 ”⟩
7 2 3 4 6 mp3an ⊢ 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2 = ⟨“ W ⁡ 0 W ⁡ 1 W ⁡ 2 ”⟩
8 1 7 eqtrdi ⊢ W ∈ Word V ∧ W = 3 → W = ⟨“ W ⁡ 0 W ⁡ 1 W ⁡ 2 ”⟩