Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-kle Unicode version

Definition df-kle 26090
Description: The Kleene star of an alphabet  x is the set of all the finite sequences of elements of this alphabet. Experimental. (Contributed by FL, 14-Jan-2014.)
Assertion
Ref Expression
df-kle  |-  Kleene  =  ( x  e.  _V  |->  U_ u  e.  NN0  ( x  ^m  ( 1 ... u ) ) )
Distinct variable group:    x, u

Detailed syntax breakdown of Definition df-kle
StepHypRef Expression
1 ckln 26083 . 2  class  Kleene
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 vu . . . 4  set  u
5 cn0 9981 . . . 4  class  NN0
62cv 1631 . . . . 5  class  x
7 c1 8754 . . . . . 6  class  1
84cv 1631 . . . . . 6  class  u
9 cfz 10798 . . . . . 6  class  ...
107, 8, 9co 5874 . . . . 5  class  ( 1 ... u )
11 cmap 6788 . . . . 5  class  ^m
126, 10, 11co 5874 . . . 4  class  ( x  ^m  ( 1 ... u ) )
134, 5, 12ciun 3921 . . 3  class  U_ u  e.  NN0  ( x  ^m  ( 1 ... u
) )
142, 3, 13cmpt 4093 . 2  class  ( x  e.  _V  |->  U_ u  e.  NN0  ( x  ^m  ( 1 ... u
) ) )
151, 14wceq 1632 1  wff  Kleene  =  ( x  e.  _V  |->  U_ u  e.  NN0  ( x  ^m  ( 1 ... u ) ) )
Colors of variables: wff set class
This definition is referenced by:  isKleene  26091
  Copyright terms: Public domain W3C validator