Definition df-word 14553

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 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word (see frmdval 18864). (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 14552	. 2 class Word 𝑆
3		cc0 11155	. . . . . 6 class 0
4		vl	. . . . . . 7 setvar 𝑙
5	4	cv 1539	. . . . . 6 class 𝑙
6		cfzo 13694	. . . . . 6 class ..^
7	3, 5, 6	co 7431	. . . . 5 class (0..^𝑙)
8		vw	. . . . . 6 setvar 𝑤
9	8	cv 1539	. . . . 5 class 𝑤
10	7, 1, 9	wf 6557	. . . 4 wff 𝑤:(0..^𝑙)⟶𝑆
11		cn0 12526	. . . 4 class ℕ0
12	10, 4, 11	wrex 3070	. . 3 wff ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆
13	12, 8	cab 2714	. 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
14	2, 13	wceq 1540	1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}

This definition is referenced by:  iswrd  14554  wrdval  14555  nfwrd  14581  csbwrdg  14582