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