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 ⊢ S ∈ V → W = ⟨“ S ”⟩ ↔ W ∈ Word V ∧ W = 1 ∧ W ⁡ 0 = S

Proof

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