Definition df-word 12664

Description: Define the class of words over a set. A word (or 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 so that two words with the same symbols in the same order will be the same. This is sometimes denoted with the Kleene star, although properly speaking that is an operator on languages. (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 12656	. 2 class Word S
3		cc0 9539	. . . . . 6 class 0
4		vl	. . . . . . 7 setvar l
5	4	cv 1443	. . . . . 6 class l
6		cfzo 11915	. . . . . 6 class ..^
7	3, 5, 6	co 6290	. . . . 5 class ( 0..^ l )
8		vw	. . . . . 6 setvar w
9	8	cv 1443	. . . . 5 class w
10	7, 1, 9	wf 5578	. . . 4 wff w : ( 0..^ l ) --> S
11		cn0 10869	. . . 4 class NN0
12	10, 4, 11	wrex 2738	. . 3 wff E. l e. NN0 w : ( 0..^ l ) --> S
13	12, 8	cab 2437	. 2 class { w | E. l e. NN0 w : ( 0..^ l ) --> S }
14	2, 13	wceq 1444	1 wff Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

This definition is referenced by:  iswrd  12672  iswrdOLD  12673  wrdval  12674  nfwrd  12695  csbwrdg  12696