Theorem repsf

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

	Ref	Expression
Assertion	repsf	|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) : ( 0 ..^ N ) --> V )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( S e. V /\ x e. ( 0 ..^ N ) ) -> S e. V )
2	1	ralrimiva	|- ( S e. V -> A. x e. ( 0 ..^ N ) S e. V )
3	2	adantr	|- ( ( S e. V /\ N e. NN0 ) -> A. x e. ( 0 ..^ N ) S e. V )
4		eqid	|- ( x e. ( 0 ..^ N ) |-> S ) = ( x e. ( 0 ..^ N ) |-> S )
5	4	fmpt	|- ( A. x e. ( 0 ..^ N ) S e. V <-> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V )
6	3 5	sylib	|- ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V )
7		reps	|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
8	7	feq1d	|- ( ( S e. V /\ N e. NN0 ) -> ( ( S repeatS N ) : ( 0 ..^ N ) --> V <-> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V ) )
9	6 8	mpbird	|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) : ( 0 ..^ N ) --> V )