Metamath Proof Explorer


Theorem repsf

Description: The constructed function mapping a half-open range of nonnegative integers to a constant is a function. (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repsf ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑆𝑉𝑥 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆𝑉 )
2 1 ralrimiva ( 𝑆𝑉 → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆𝑉 )
3 2 adantr ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆𝑉 )
4 eqid ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 )
5 4 fmpt ( ∀ 𝑥 ∈ ( 0 ..^ 𝑁 ) 𝑆𝑉 ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
6 3 5 sylib ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
7 reps ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
8 7 feq1d ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 ) )
9 6 8 mpbird ( ( 𝑆𝑉𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )