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

Metamath Proof Explorer

Theorem wrdlen2s2

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

Ref Expression
Assertion wrdlen2s2 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )

Proof

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