Definition df-word 11678

Description: Define the class of words over a set. A word is a finite sequence of symbols from a set. 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 11672	. 2 class Word S
3		cc0 8946	. . . . . 6 class 0
4		vl	. . . . . . 7 set l
5	4	cv 1648	. . . . . 6 class l
6		cfzo 11090	. . . . . 6 class ..^
7	3, 5, 6	co 6040	. . . . 5 class ( 0..^ l )
8		vw	. . . . . 6 set w
9	8	cv 1648	. . . . 5 class w
10	7, 1, 9	wf 5409	. . . 4 wff w : ( 0..^ l ) --> S
11		cn0 10177	. . . 4 class NN0
12	10, 4, 11	wrex 2667	. . 3 wff E. l e. NN0 w : ( 0..^ l ) --> S
13	12, 8	cab 2390	. 2 class { w | E. l e. NN0 w : ( 0..^ l ) --> S }
14	2, 13	wceq 1649	1 wff Word S = { w | E. l e. NN0 w : ( 0..^ l ) --> S }

This definition is referenced by:  iswrd  11684  wrdval  11685  nfwrd  11695