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