Metamath Proof Explorer

Theorem wrdl1exs1

Description: A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021)

Ref Expression
Assertion wrdl1exs1 ⊢ W ∈ Word S ∧ W = 1 → ∃ s ∈ S W = ⟨“ s ”⟩

Proof

Step Hyp Ref Expression
1 1le1 ⊢ 1 ≤ 1
2 breq2 ⊢ W = 1 → 1 ≤ W ↔ 1 ≤ 1
3 1 2 mpbiri ⊢ W = 1 → 1 ≤ W
4 wrdsymb1 ⊢ W ∈ Word S ∧ 1 ≤ W → W ⁡ 0 ∈ S
5 3 4 sylan2 ⊢ W ∈ Word S ∧ W = 1 → W ⁡ 0 ∈ S
6 s1eq ⊢ s = W ⁡ 0 → ⟨“ s ”⟩ = ⟨“ W ⁡ 0 ”⟩
7 6 adantl ⊢ W ∈ Word S ∧ W = 1 ∧ s = W ⁡ 0 → ⟨“ s ”⟩ = ⟨“ W ⁡ 0 ”⟩
8 7 eqeq2d ⊢ W ∈ Word S ∧ W = 1 ∧ s = W ⁡ 0 → W = ⟨“ s ”⟩ ↔ W = ⟨“ W ⁡ 0 ”⟩
9 eqs1 ⊢ W ∈ Word S ∧ W = 1 → W = ⟨“ W ⁡ 0 ”⟩
10 5 8 9 rspcedvd ⊢ W ∈ Word S ∧ W = 1 → ∃ s ∈ S W = ⟨“ s ”⟩