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	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}N=\left(0..^N\right)\times \left\{S\right\}$$

Proof

Step	Hyp	Ref	Expression
1		reps	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}N=\left(x\in \left(0..^N\right)⟼S\right)$$
2		fconstmpt	$$⊢\left(0..^N\right)\times \left\{S\right\}=\left(x\in \left(0..^N\right)⟼S\right)$$
3	1 2	eqtr4di	$$⊢\left(S\in V\wedge N\in {\mathbb{N}}_0\right)\to S\mathrm{repeatS}N=\left(0..^N\right)\times \left\{S\right\}$$