Metamath Proof Explorer


Definition df-reps

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)

Ref Expression
Assertion df-reps repeatS = ( 𝑠 ∈ V , 𝑛 ∈ ℕ0 ↦ ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 creps repeatS
1 vs 𝑠
2 cvv V
3 vn 𝑛
4 cn0 0
5 vx 𝑥
6 cc0 0
7 cfzo ..^
8 3 cv 𝑛
9 6 8 7 co ( 0 ..^ 𝑛 )
10 1 cv 𝑠
11 5 9 10 cmpt ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 )
12 1 3 2 4 11 cmpo ( 𝑠 ∈ V , 𝑛 ∈ ℕ0 ↦ ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) )
13 0 12 wceq repeatS = ( 𝑠 ∈ V , 𝑛 ∈ ℕ0 ↦ ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) )