This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ..^ 𝑁 ) ↦ 𝑆 ) )