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

Definition df-word 11723
 Description: Define the class of words over a set. A word is a 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 ..^
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-word
StepHypRef Expression
1 cS . . 3
21cword 11717 . 2 Word
3 cc0 8990 . . . . . 6
4 vl . . . . . . 7
54cv 1651 . . . . . 6
6 cfzo 11135 . . . . . 6 ..^
73, 5, 6co 6081 . . . . 5 ..^
8 vw . . . . . 6
98cv 1651 . . . . 5
107, 1, 9wf 5450 . . . 4 ..^
11 cn0 10221 . . . 4
1210, 4, 11wrex 2706 . . 3 ..^
1312, 8cab 2422 . 2 ..^
142, 13wceq 1652 1 Word ..^
 Colors of variables: wff set class This definition is referenced by:  iswrd  11729  wrdval  11730  nfwrd  11740
 Copyright terms: Public domain W3C validator