Metamath Proof Explorer

Theorem pfxf

Description: A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxf ⊢ W ∈ Word V ∧ L ∈ 0 … W → W prefix L : 0 ..^ L ⟶ V

Proof

Step Hyp Ref Expression
1 pfxmpt ⊢ W ∈ Word V ∧ L ∈ 0 … W → W prefix L = x ∈ 0 ..^ L ⟼ W ⁡ x
2 simpll ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ x ∈ 0 ..^ L → W ∈ Word V
3 elfzuz3 ⊢ L ∈ 0 … W → W ∈ ℤ ≥ L
4 3 adantl ⊢ W ∈ Word V ∧ L ∈ 0 … W → W ∈ ℤ ≥ L
5 fzoss2 ⊢ W ∈ ℤ ≥ L → 0 ..^ L ⊆ 0 ..^ W
6 4 5 syl ⊢ W ∈ Word V ∧ L ∈ 0 … W → 0 ..^ L ⊆ 0 ..^ W
7 6 sselda ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ x ∈ 0 ..^ L → x ∈ 0 ..^ W
8 wrdsymbcl ⊢ W ∈ Word V ∧ x ∈ 0 ..^ W → W ⁡ x ∈ V
9 2 7 8 syl2anc ⊢ W ∈ Word V ∧ L ∈ 0 … W ∧ x ∈ 0 ..^ L → W ⁡ x ∈ V
10 1 9 fmpt3d ⊢ W ∈ Word V ∧ L ∈ 0 … W → W prefix L : 0 ..^ L ⟶ V