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 13492
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 13484 . 2 class repeatS
2 vs . . 3 setvar 𝑠
3 vn . . 3 setvar 𝑛
4 cvv 3340 . . 3 class V
5 cn0 11484 . . 3 class 0
6 vx . . . 4 setvar 𝑥
7 cc0 10128 . . . . 5 class 0
83cv 1631 . . . . 5 class 𝑛
9 cfzo 12659 . . . . 5 class ..^
107, 8, 9co 6813 . . . 4 class (0..^𝑛)
112cv 1631 . . . 4 class 𝑠
126, 10, 11cmpt 4881 . . 3 class (𝑥 ∈ (0..^𝑛) ↦ 𝑠)
132, 3, 4, 5, 12cmpt2 6815 . 2 class (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
141, 13wceq 1632 1 wff repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
Colors of variables: wff setvar class
This definition is referenced by:  reps  13717  repsundef  13718
  Copyright terms: Public domain W3C validator