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

Metamath Proof Explorer

Theorem wrdl1s1

Description: A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 s1cl ⊢ ( 𝑆 ∈ 𝑉 → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
2 s1len ⊢ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1
3 2 a1i ⊢ ( 𝑆 ∈ 𝑉 → ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 )
4 s1fv ⊢ ( 𝑆 ∈ 𝑉 → ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 )
5 1 3 4 3jca ⊢ ( 𝑆 ∈ 𝑉 → ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
6 eleq1 ⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ↔ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) )
7 fveqeq2 ⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( ♯ ‘ 𝑊 ) = 1 ↔ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ) )
8 fveq1 ⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ‘ 0 ) = ( ⟨“ 𝑆 ”⟩ ‘ 0 ) )
9 8 eqeq1d ⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ‘ 0 ) = 𝑆 ↔ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
10 6 7 9 3anbi123d ⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ↔ ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) ) )
11 5 10 syl5ibrcom ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )
12 eqs1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
13 s1eq ⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ⟨“ 𝑆 ”⟩ )
14 13 eqeq2d ⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ↔ 𝑊 = ⟨“ 𝑆 ”⟩ ) )
15 12 14 syl5ibcom ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑆 → 𝑊 = ⟨“ 𝑆 ”⟩ ) )
16 15 3impia ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) → 𝑊 = ⟨“ 𝑆 ”⟩ )
17 11 16 impbid1 ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )