Metamath Proof Explorer

Theorem repswfsts

Description: The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repswfsts ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ⁡ 0 = S

Proof

Step Hyp Ref Expression
1 simpl ⊢ S ∈ V ∧ N ∈ ℕ → S ∈ V
2 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
3 2 adantl ⊢ S ∈ V ∧ N ∈ ℕ → N ∈ ℕ 0
4 lbfzo0 ⊢ 0 ∈ 0 ..^ N ↔ N ∈ ℕ
5 4 bilanri ⊢ S ∈ V ∧ N ∈ ℕ → 0 ∈ 0 ..^ N
6 repswsymb ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ 0 ∈ 0 ..^ N → S repeatS N ⁡ 0 = S
7 1 3 5 6 syl3anc ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ⁡ 0 = S