Metamath Proof Explorer

Theorem repsconst

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

		Ref	Expression
	Assertion	repsconst	\|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0 ..^ N ) X. { S } ) )

Proof

Step	Hyp	Ref	Expression
1		reps	\|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) \|-> S ) )
2		fconstmpt	\|- ( ( 0 ..^ N ) X. { S } ) = ( x e. ( 0 ..^ N ) \|-> S )
3	1 2	eqtr4di	\|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0 ..^ N ) X. { S } ) )

Step

Hyp

Ref

Expression

reps

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

fconstmpt

 |-  ( ( 0 ..^ N ) X. { S } ) = ( x e. ( 0 ..^ N ) |-> S )

1 2

eqtr4di

 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( ( 0 ..^ N ) X. { S } ) )