MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-word Structured version   Visualization version   Unicode version

Definition df-word 12711
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
StepHypRef Expression
1 cS . . 3  class  S
21cword 12703 . 2  class Word  S
3 cc0 9557 . . . . . 6  class  0
4 vl . . . . . . 7  setvar  l
54cv 1451 . . . . . 6  class  l
6 cfzo 11942 . . . . . 6  class ..^
73, 5, 6co 6308 . . . . 5  class  ( 0..^ l )
8 vw . . . . . 6  setvar  w
98cv 1451 . . . . 5  class  w
107, 1, 9wf 5585 . . . 4  wff  w : ( 0..^ l ) --> S
11 cn0 10893 . . . 4  class  NN0
1210, 4, 11wrex 2757 . . 3  wff  E. l  e.  NN0  w : ( 0..^ l ) --> S
1312, 8cab 2457 . 2  class  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
142, 13wceq 1452 1  wff Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
Colors of variables: wff setvar class
This definition is referenced by:  iswrd  12719  iswrdOLD  12720  wrdval  12721  nfwrd  12746  csbwrdg  12747
  Copyright terms: Public domain W3C validator