Definition df-pfx 14027

Description: Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, (𝑆 prefix 𝐿) is the prefix of the word 𝑆 of length 𝐿. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (Contributed by AV, 2-May-2020.)

Assertion

Ref	Expression
df-pfx	⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))

Distinct variable group:   𝑠,𝑙

Detailed syntax breakdown of Definition df-pfx

Step	Hyp	Ref	Expression
1		cpfx 14026	. 2 class prefix
2		vs	. . 3 setvar 𝑠
3		vl	. . 3 setvar 𝑙
4		cvv 3494	. . 3 class V
5		cn0 11891	. . 3 class ℕ0
6	2	cv 1532	. . . 4 class 𝑠
7		cc0 10531	. . . . 5 class 0
8	3	cv 1532	. . . . 5 class 𝑙
9	7, 8	cop 4566	. . . 4 class ⟨0, 𝑙⟩
10		csubstr 13996	. . . 4 class substr
11	6, 9, 10	co 7150	. . 3 class (𝑠 substr ⟨0, 𝑙⟩)
12	2, 3, 4, 5, 11	cmpo 7152	. 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
13	1, 12	wceq 1533	1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))

This definition is referenced by:  pfxnndmnd  14028  pfxval  14029  pfx00  14030  pfx0  14031  pfxcl  14033