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	$$⊢\mathrm{repeatS}=\left(s\in \mathrm{V},n\in {\mathbb{N}}_0⟼\left(x\in \left(0..^n\right)⟼s\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creps	$$class\mathrm{repeatS}$$
1		vs	$$setvars$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5		vx	$$setvarx$$
6		cc0	$$class0$$
7		cfzo	$$class..^$$
8	3	cv	$$setvarn$$
9	6 8 7	co	$$class\left(0..^n\right)$$
10	1	cv	$$setvars$$
11	5 9 10	cmpt	$$class\left(x\in \left(0..^n\right)⟼s\right)$$
12	1 3 2 4 11	cmpo	$$class\left(s\in \mathrm{V},n\in {\mathbb{N}}_0⟼\left(x\in \left(0..^n\right)⟼s\right)\right)$$
13	0 12	wceq	$$wff\mathrm{repeatS}=\left(s\in \mathrm{V},n\in {\mathbb{N}}_0⟼\left(x\in \left(0..^n\right)⟼s\right)\right)$$