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

Definition df-word 13852
 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) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ0 so that two words with the same symbols in the same order be equal. The set Word 𝑆 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 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17999). (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 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Distinct variable group:   𝑤,𝑙,𝑆

Detailed syntax breakdown of Definition df-word
StepHypRef Expression
1 cS . . 3 class 𝑆
21cword 13851 . 2 class Word 𝑆
3 cc0 10526 . . . . . 6 class 0
4 vl . . . . . . 7 setvar 𝑙
54cv 1529 . . . . . 6 class 𝑙
6 cfzo 13023 . . . . . 6 class ..^
73, 5, 6co 7148 . . . . 5 class (0..^𝑙)
8 vw . . . . . 6 setvar 𝑤
98cv 1529 . . . . 5 class 𝑤
107, 1, 9wf 6348 . . . 4 wff 𝑤:(0..^𝑙)⟶𝑆
11 cn0 11886 . . . 4 class 0
1210, 4, 11wrex 3144 . . 3 wff 𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆
1312, 8cab 2804 . 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
142, 13wceq 1530 1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
 Colors of variables: wff setvar class This definition is referenced by:  iswrd  13853  wrdval  13854  nfwrd  13884  csbwrdg  13885
 Copyright terms: Public domain W3C validator