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

Definition df-reps 12511
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 12503 . 2  class repeatS
2 vs . . 3  setvar  s
3 vn . . 3  setvar  n
4 cvv 3113 . . 3  class  _V
5 cn0 10791 . . 3  class  NN0
6 vx . . . 4  setvar  x
7 cc0 9488 . . . . 5  class  0
83cv 1378 . . . . 5  class  n
9 cfzo 11788 . . . . 5  class ..^
107, 8, 9co 6282 . . . 4  class  ( 0..^ n )
112cv 1378 . . . 4  class  s
126, 10, 11cmpt 4505 . . 3  class  ( x  e.  ( 0..^ n )  |->  s )
132, 3, 4, 5, 12cmpt2 6284 . 2  class  ( s  e.  _V ,  n  e.  NN0  |->  ( x  e.  ( 0..^ n ) 
|->  s ) )
141, 13wceq 1379 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  12701  repsundef  12702
  Copyright terms: Public domain W3C validator