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

Definition df-word 13096
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) 𝑆. 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 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Distinct variable group:   𝑤,𝑙,𝑆

Detailed syntax breakdown of Definition df-word
StepHypRef Expression
1 cS . . 3 class 𝑆
21cword 13088 . 2 class Word 𝑆
3 cc0 9788 . . . . . 6 class 0
4 vl . . . . . . 7 setvar 𝑙
54cv 1473 . . . . . 6 class 𝑙
6 cfzo 12285 . . . . . 6 class ..^
73, 5, 6co 6523 . . . . 5 class (0..^𝑙)
8 vw . . . . . 6 setvar 𝑤
98cv 1473 . . . . 5 class 𝑤
107, 1, 9wf 5782 . . . 4 wff 𝑤:(0..^𝑙)⟶𝑆
11 cn0 11135 . . . 4 class 0
1210, 4, 11wrex 2892 . . 3 wff 𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆
1312, 8cab 2591 . 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
142, 13wceq 1474 1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Colors of variables: wff setvar class
This definition is referenced by:  iswrd  13104  wrdval  13105  nfwrd  13130  csbwrdg  13131
  Copyright terms: Public domain W3C validator