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 ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N : 0 ..^ N ⟶ V

Proof

Step Hyp Ref Expression
1 simpl ⊢ S ∈ V ∧ x ∈ 0 ..^ N → S ∈ V
2 1 ralrimiva ⊢ S ∈ V → ∀ x ∈ 0 ..^ N S ∈ V
3 2 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 → ∀ x ∈ 0 ..^ N S ∈ V
4 eqid ⊢ x ∈ 0 ..^ N ⟼ S = x ∈ 0 ..^ N ⟼ S
5 4 fmpt ⊢ ∀ x ∈ 0 ..^ N S ∈ V ↔ x ∈ 0 ..^ N ⟼ S : 0 ..^ N ⟶ V
6 3 5 sylib ⊢ S ∈ V ∧ N ∈ ℕ 0 → x ∈ 0 ..^ N ⟼ S : 0 ..^ N ⟶ V
7 reps ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N = x ∈ 0 ..^ N ⟼ S
8 7 feq1d ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N : 0 ..^ N ⟶ V ↔ x ∈ 0 ..^ N ⟼ S : 0 ..^ N ⟶ V
9 6 8 mpbird ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N : 0 ..^ N ⟶ V