Theorem reps

Description: Construct a function mapping a half-open range of nonnegative integers to a constant. (Contributed by AV, 4-Nov-2018)

	Ref	Expression
Assertion	reps	|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( S e. V -> S e. _V )
2	1	adantr	|- ( ( S e. V /\ N e. NN0 ) -> S e. _V )
3		simpr	|- ( ( S e. V /\ N e. NN0 ) -> N e. NN0 )
4		ovex	|- ( 0 ..^ N ) e. _V
5		mptexg	|- ( ( 0 ..^ N ) e. _V -> ( x e. ( 0 ..^ N ) |-> S ) e. _V )
6	4 5	mp1i	|- ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ N ) |-> S ) e. _V )
7		oveq2	|- ( n = N -> ( 0 ..^ n ) = ( 0 ..^ N ) )
8	7	adantl	|- ( ( s = S /\ n = N ) -> ( 0 ..^ n ) = ( 0 ..^ N ) )
9		simpll	|- ( ( ( s = S /\ n = N ) /\ x e. ( 0 ..^ n ) ) -> s = S )
10	8 9	mpteq12dva	|- ( ( s = S /\ n = N ) -> ( x e. ( 0 ..^ n ) |-> s ) = ( x e. ( 0 ..^ N ) |-> S ) )
11		df-reps	|- repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) )
12	10 11	ovmpoga	|- ( ( S e. _V /\ N e. NN0 /\ ( x e. ( 0 ..^ N ) |-> S ) e. _V ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
13	2 3 6 12	syl3anc	|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )