Definition df-word 10915

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) S. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of NN0 so that two words with the same symbols in the same order be equal. The set Word S 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 S equipped with concatenation is the free monoid over S, and the monoid unit is the empty word. (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 S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

Distinct variable group:   w, l, S

Detailed syntax breakdown of Definition df-word

Step	Hyp	Ref	Expression
1		cS	. . 3 class S
2	1	cword 10914	. 2 class Word S
3		cc0 7872	. . . . . 6 class 0
4		vl	. . . . . . 7 setvar l
5	4	cv 1363	. . . . . 6 class l
6		cfzo 10208	. . . . . 6 class ..^
7	3, 5, 6	co 5918	. . . . 5 class ( 0..^ l )
8		vw	. . . . . 6 setvar w
9	8	cv 1363	. . . . 5 class w
10	7, 1, 9	wf 5250	. . . 4 wff w : ( 0..^ l ) --> S
11		cn0 9240	. . . 4 class NN0
12	10, 4, 11	wrex 2473	. . 3 wff E. l e. NN0 w : ( 0..^ l ) --> S
13	12, 8	cab 2179	. 2 class { w | E. l e. NN0 w : ( 0..^ l ) --> S }
14	2, 13	wceq 1364	1 wff Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

This definition is referenced by:  iswrd  10916  wrdval  10917  nfwrd  10942  csbwrdg  10943