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

Definition df-reps 14110
 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 14109 . 2 class repeatS
2 vs . . 3 setvar 𝑠
3 vn . . 3 setvar 𝑛
4 cvv 3471 . . 3 class V
5 cn0 11875 . . 3 class 0
6 vx . . . 4 setvar 𝑥
7 cc0 10514 . . . . 5 class 0
83cv 1537 . . . . 5 class 𝑛
9 cfzo 13016 . . . . 5 class ..^
107, 8, 9co 7130 . . . 4 class (0..^𝑛)
112cv 1537 . . . 4 class 𝑠
126, 10, 11cmpt 5119 . . 3 class (𝑥 ∈ (0..^𝑛) ↦ 𝑠)
132, 3, 4, 5, 12cmpo 7132 . 2 class (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
141, 13wceq 1538 1 wff repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
 Colors of variables: wff setvar class This definition is referenced by:  reps  14111  repsundef  14112
 Copyright terms: Public domain W3C validator