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 ”⟩