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

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 imbitrrid ⊢ ( 𝑊 ∈ Word 𝐴 → ( ( ♯ ‘ 𝑊 ) = 1 → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) )
24 23 imp ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )