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

Definition df-reps 12324
Description: Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.)
Assertion
Ref Expression
df-reps  |- repeatS  =  ( s  e.  _V ,  n  e.  NN0  |->  ( x  e.  ( 0..^ n )  |->  s ) )
Distinct variable group:    n, s, x

Detailed syntax breakdown of Definition df-reps
StepHypRef Expression
1 creps 12316 . 2  class repeatS
2 vs . . 3  setvar  s
3 vn . . 3  setvar  n
4 cvv 3054 . . 3  class  _V
5 cn0 10666 . . 3  class  NN0
6 vx . . . 4  setvar  x
7 cc0 9369 . . . . 5  class  0
83cv 1369 . . . . 5  class  n
9 cfzo 11635 . . . . 5  class ..^
107, 8, 9co 6176 . . . 4  class  ( 0..^ n )
112cv 1369 . . . 4  class  s
126, 10, 11cmpt 4434 . . 3  class  ( x  e.  ( 0..^ n )  |->  s )
132, 3, 4, 5, 12cmpt2 6178 . 2  class  ( s  e.  _V ,  n  e.  NN0  |->  ( x  e.  ( 0..^ n ) 
|->  s ) )
141, 13wceq 1370 1  wff repeatS  =  ( s  e.  _V ,  n  e.  NN0  |->  ( x  e.  ( 0..^ n )  |->  s ) )
Colors of variables: wff setvar class
This definition is referenced by:  reps  12496  repsundef  12497
  Copyright terms: Public domain W3C validator