Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-word | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-word | ⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cS | . . 3 class 𝑆 | |
2 | 1 | cword 13146 | . 2 class Word 𝑆 |
3 | cc0 9815 | . . . . . 6 class 0 | |
4 | vl | . . . . . . 7 setvar 𝑙 | |
5 | 4 | cv 1474 | . . . . . 6 class 𝑙 |
6 | cfzo 12334 | . . . . . 6 class ..^ | |
7 | 3, 5, 6 | co 6549 | . . . . 5 class (0..^𝑙) |
8 | vw | . . . . . 6 setvar 𝑤 | |
9 | 8 | cv 1474 | . . . . 5 class 𝑤 |
10 | 7, 1, 9 | wf 5800 | . . . 4 wff 𝑤:(0..^𝑙)⟶𝑆 |
11 | cn0 11169 | . . . 4 class ℕ0 | |
12 | 10, 4, 11 | wrex 2897 | . . 3 wff ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆 |
13 | 12, 8 | cab 2596 | . 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
14 | 2, 13 | wceq 1475 | 1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆} |
Colors of variables: wff setvar class |
This definition is referenced by: iswrd 13162 wrdval 13163 nfwrd 13188 csbwrdg 13189 |
Copyright terms: Public domain | W3C validator |