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

Definition df-word 11409
Description: Define the class of words over a set. A word is an 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
StepHypRef Expression
1 cS . . 3  class  S
21cword 11403 . 2  class Word  S
3 cc0 8737 . . . . . 6  class  0
4 vl . . . . . . 7  set  l
54cv 1622 . . . . . 6  class  l
6 cfzo 10870 . . . . . 6  class ..^
73, 5, 6co 5858 . . . . 5  class  ( 0..^ l )
8 vw . . . . . 6  set  w
98cv 1622 . . . . 5  class  w
107, 1, 9wf 5251 . . . 4  wff  w : ( 0..^ l ) --> S
11 cn0 9965 . . . 4  class  NN0
1210, 4, 11wrex 2544 . . 3  wff  E. l  e.  NN0  w : ( 0..^ l ) --> S
1312, 8cab 2269 . 2  class  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
142, 13wceq 1623 1  wff Word  S  =  { w  |  E. l  e.  NN0  w : ( 0..^ l ) --> S }
Colors of variables: wff set class
This definition is referenced by:  iswrd  11415  wrdval  11416  nfwrd  11426
  Copyright terms: Public domain W3C validator