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

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 ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ∃ 𝑠 ∈ 𝑆 𝑊 = ⟨“ 𝑠 ”⟩ )

Proof

Step Hyp Ref Expression
1 1le1 ⊢ 1 ≤ 1
2 breq2 ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 1 ) )
3 1 2 mpbiri ⊢ ( ( ♯ ‘ 𝑊 ) = 1 → 1 ≤ ( ♯ ‘ 𝑊 ) )
4 wrdsymb1 ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑆 )
5 3 4 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 ‘ 0 ) ∈ 𝑆 )
6 s1eq ⊢ ( 𝑠 = ( 𝑊 ‘ 0 ) → ⟨“ 𝑠 ”⟩ = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
7 6 adantl ⊢ ( ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) ∧ 𝑠 = ( 𝑊 ‘ 0 ) ) → ⟨“ 𝑠 ”⟩ = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
8 7 eqeq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) ∧ 𝑠 = ( 𝑊 ‘ 0 ) ) → ( 𝑊 = ⟨“ 𝑠 ”⟩ ↔ 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) )
9 eqs1 ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
10 5 8 9 rspcedvd ⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ∃ 𝑠 ∈ 𝑆 𝑊 = ⟨“ 𝑠 ”⟩ )