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

Definition df-reps 12531
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 12523 . 2  class repeatS
2 vs . . 3  setvar  s
3 vn . . 3  setvar  n
4 cvv 3095 . . 3  class  _V
5 cn0 10802 . . 3  class  NN0
6 vx . . . 4  setvar  x
7 cc0 9495 . . . . 5  class  0
83cv 1382 . . . . 5  class  n
9 cfzo 11806 . . . . 5  class ..^
107, 8, 9co 6281 . . . 4  class  ( 0..^ n )
112cv 1382 . . . 4  class  s
126, 10, 11cmpt 4495 . . 3  class  ( x  e.  ( 0..^ n )  |->  s )
132, 3, 4, 5, 12cmpt2 6283 . 2  class  ( s  e.  _V ,  n  e.  NN0  |->  ( x  e.  ( 0..^ n ) 
|->  s ) )
141, 13wceq 1383 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  12724  repsundef  12725
  Copyright terms: Public domain W3C validator