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

Definition df-reps 13110
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 = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
Distinct variable group:   𝑛,𝑠,𝑥

Detailed syntax breakdown of Definition df-reps
StepHypRef Expression
1 creps 13102 . 2 class repeatS
2 vs . . 3 setvar 𝑠
3 vn . . 3 setvar 𝑛
4 cvv 3173 . . 3 class V
5 cn0 11142 . . 3 class 0
6 vx . . . 4 setvar 𝑥
7 cc0 9793 . . . . 5 class 0
83cv 1474 . . . . 5 class 𝑛
9 cfzo 12292 . . . . 5 class ..^
107, 8, 9co 6527 . . . 4 class (0..^𝑛)
112cv 1474 . . . 4 class 𝑠
126, 10, 11cmpt 4638 . . 3 class (𝑥 ∈ (0..^𝑛) ↦ 𝑠)
132, 3, 4, 5, 12cmpt2 6529 . 2 class (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
141, 13wceq 1475 1 wff repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
Colors of variables: wff setvar class
This definition is referenced by:  reps  13317  repsundef  13318
  Copyright terms: Public domain W3C validator