Theorem repsw1

Description: The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018)

	Ref	Expression
Assertion	repsw1	|- ( S e. V -> ( S repeatS 1 ) = <" S "> )

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		repsconst	|- ( ( S e. V /\ 1 e. NN0 ) -> ( S repeatS 1 ) = ( ( 0 ..^ 1 ) X. { S } ) )
3	1 2	mpan2	|- ( S e. V -> ( S repeatS 1 ) = ( ( 0 ..^ 1 ) X. { S } ) )
4		fzo01	|- ( 0 ..^ 1 ) = { 0 }
5	4	a1i	|- ( S e. V -> ( 0 ..^ 1 ) = { 0 } )
6	5	xpeq1d	|- ( S e. V -> ( ( 0 ..^ 1 ) X. { S } ) = ( { 0 } X. { S } ) )
7		c0ex	|- 0 e. _V
8		xpsng	|- ( ( 0 e. _V /\ S e. V ) -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
9	7 8	mpan	|- ( S e. V -> ( { 0 } X. { S } ) = { <. 0 , S >. } )
10	3 6 9	3eqtrd	|- ( S e. V -> ( S repeatS 1 ) = { <. 0 , S >. } )
11		s1val	|- ( S e. V -> <" S "> = { <. 0 , S >. } )
12	10 11	eqtr4d	|- ( S e. V -> ( S repeatS 1 ) = <" S "> )