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