Definition df-word 13575

Description: Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ₀ so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17742). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-word	⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}

Distinct variable group:   𝑤,𝑙,𝑆

Detailed syntax breakdown of Definition df-word

Step	Hyp	Ref	Expression
1		cS	. . 3 class 𝑆
2	1	cword 13574	. 2 class Word 𝑆
3		cc0 10252	. . . . . 6 class 0
4		vl	. . . . . . 7 setvar 𝑙
5	4	cv 1657	. . . . . 6 class 𝑙
6		cfzo 12760	. . . . . 6 class ..^
7	3, 5, 6	co 6905	. . . . 5 class (0..^𝑙)
8		vw	. . . . . 6 setvar 𝑤
9	8	cv 1657	. . . . 5 class 𝑤
10	7, 1, 9	wf 6119	. . . 4 wff 𝑤:(0..^𝑙)⟶𝑆
11		cn0 11618	. . . 4 class ℕ0
12	10, 4, 11	wrex 3118	. . 3 wff ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆
13	12, 8	cab 2811	. 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
14	2, 13	wceq 1658	1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}

This definition is referenced by:  iswrd  13576  wrdval  13577  nfwrd  13603  csbwrdg  13604