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

Metamath Proof Explorer

Theorem wrdred1

Description: A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021)

Ref Expression
Assertion wrdred1 ( 𝐹 ∈ Word 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )

Proof

Step Hyp Ref Expression
1 wrdf ⊢ ( 𝐹 ∈ Word 𝑆 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 )
2 lencl ⊢ ( 𝐹 ∈ Word 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
3 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
4 fzossrbm1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
5 3 4 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6 fssres ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 )
7 5 6 sylan2 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 )
8 iswrdi ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )
9 7 8 syl ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )
10 1 2 9 syl2anc ⊢ ( 𝐹 ∈ Word 𝑆 → ( 𝐹 ↾ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Word 𝑆 )