This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ( 𝑊 ‘ 2 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 wrd3tpop ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 = { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ , ⟨ 2 , ( 𝑊 ‘ 2 ) ⟩ } )
2 fvex ⊢ ( 𝑊 ‘ 0 ) ∈ V
3 fvex ⊢ ( 𝑊 ‘ 1 ) ∈ V
4 fvex ⊢ ( 𝑊 ‘ 2 ) ∈ V
5 s3tpop ⊢ ( ( ( 𝑊 ‘ 0 ) ∈ V ∧ ( 𝑊 ‘ 1 ) ∈ V ∧ ( 𝑊 ‘ 2 ) ∈ V ) → ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ( 𝑊 ‘ 2 ) ”⟩ = { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ , ⟨ 2 , ( 𝑊 ‘ 2 ) ⟩ } )
6 5 eqcomd ⊢ ( ( ( 𝑊 ‘ 0 ) ∈ V ∧ ( 𝑊 ‘ 1 ) ∈ V ∧ ( 𝑊 ‘ 2 ) ∈ V ) → { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ , ⟨ 2 , ( 𝑊 ‘ 2 ) ⟩ } = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ( 𝑊 ‘ 2 ) ”⟩ )
7 2 3 4 6 mp3an ⊢ { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ , ⟨ 2 , ( 𝑊 ‘ 2 ) ⟩ } = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ( 𝑊 ‘ 2 ) ”⟩
8 1 7 eqtrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ( 𝑊 ‘ 2 ) ”⟩ )