This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ..^ 𝑛 ) ↦ 𝑠 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creps	⊢ repeatS
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cn0	⊢ ℕ₀
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 ..^ 𝑛 ) ↦ 𝑠 ) )
13	0 12	wceq	⊢ repeatS = ( 𝑠 ∈ V , 𝑛 ∈ ℕ₀ ↦ ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) )