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 14480
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 14479 . 2 class repeatS
2 vs . . 3 setvar 𝑠
3 vn . . 3 setvar 𝑛
4 cvv 3431 . . 3 class V
5 cn0 12233 . . 3 class 0
6 vx . . . 4 setvar 𝑥
7 cc0 10872 . . . . 5 class 0
83cv 1541 . . . . 5 class 𝑛
9 cfzo 13381 . . . . 5 class ..^
107, 8, 9co 7271 . . . 4 class (0..^𝑛)
112cv 1541 . . . 4 class 𝑠
126, 10, 11cmpt 5162 . . 3 class (𝑥 ∈ (0..^𝑛) ↦ 𝑠)
132, 3, 4, 5, 12cmpo 7273 . 2 class (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
141, 13wceq 1542 1 wff repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠))
Colors of variables: wff setvar class
This definition is referenced by:  reps  14481  repsundef  14482
  Copyright terms: Public domain W3C validator