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	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
2	1	adantr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑆 ∈ V )
3		simpr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
4		ovex	⊢ ( 0 ..^ 𝑁 ) ∈ V
5		mptexg	⊢ ( ( 0 ..^ 𝑁 ) ∈ V → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) ∈ V )
6	4 5	mp1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) ∈ V )
7		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ..^ 𝑛 ) = ( 0 ..^ 𝑁 ) )
8	7	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑛 = 𝑁 ) → ( 0 ..^ 𝑛 ) = ( 0 ..^ 𝑁 ) )
9		simpll	⊢ ( ( ( 𝑠 = 𝑆 ∧ 𝑛 = 𝑁 ) ∧ 𝑥 ∈ ( 0 ..^ 𝑛 ) ) → 𝑠 = 𝑆 )
10	8 9	mpteq12dva	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑛 = 𝑁 ) → ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
11		df-reps	⊢ repeatS = ( 𝑠 ∈ V , 𝑛 ∈ ℕ0 ↦ ( 𝑥 ∈ ( 0 ..^ 𝑛 ) ↦ 𝑠 ) )
12	10 11	ovmpoga	⊢ ( ( 𝑆 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) ∈ V ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
13	2 3 6 12	syl3anc	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )