Metamath Proof Explorer


Theorem eqs1

Description: A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion eqs1 ( ( 𝑊 ∈ Word 𝐴 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )

Proof

Step Hyp Ref Expression
1 id ( ( ♯ ‘ 𝑊 ) = 1 → ( ♯ ‘ 𝑊 ) = 1 )
2 s1len ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) = 1
3 1 2 eqtr4di ( ( ♯ ‘ 𝑊 ) = 1 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) )
4 fvex ( 𝑊 ‘ 0 ) ∈ V
5 s1fv ( ( 𝑊 ‘ 0 ) ∈ V → ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 ) = ( 𝑊 ‘ 0 ) )
6 4 5 ax-mp ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 ) = ( 𝑊 ‘ 0 )
7 6 eqcomi ( 𝑊 ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 )
8 c0ex 0 ∈ V
9 fveq2 ( 𝑥 = 0 → ( 𝑊𝑥 ) = ( 𝑊 ‘ 0 ) )
10 fveq2 ( 𝑥 = 0 → ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 ) )
11 9 10 eqeq12d ( 𝑥 = 0 → ( ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ↔ ( 𝑊 ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 ) ) )
12 8 11 ralsn ( ∀ 𝑥 ∈ { 0 } ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ↔ ( 𝑊 ‘ 0 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 0 ) )
13 7 12 mpbir 𝑥 ∈ { 0 } ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 )
14 oveq2 ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 1 ) )
15 fzo01 ( 0 ..^ 1 ) = { 0 }
16 14 15 eqtrdi ( ( ♯ ‘ 𝑊 ) = 1 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = { 0 } )
17 16 raleqdv ( ( ♯ ‘ 𝑊 ) = 1 → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ { 0 } ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ) )
18 13 17 mpbiri ( ( ♯ ‘ 𝑊 ) = 1 → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) )
19 3 18 jca ( ( ♯ ‘ 𝑊 ) = 1 → ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ) )
20 s1cli ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V
21 eqwrd ( ( 𝑊 ∈ Word 𝐴 ∧ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ∈ Word V ) → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ) ) )
22 20 21 mpan2 ( 𝑊 ∈ Word 𝐴 → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ↔ ( ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊𝑥 ) = ( ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ‘ 𝑥 ) ) ) )
23 19 22 syl5ibr ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) = 1 → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) )
24 23 imp ( ( 𝑊 ∈ Word 𝐴 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )