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

Metamath Proof Explorer

Theorem fvffz0

Description: The function value of a function from a finite interval of nonnegative integers. (Contributed by AV, 13-Feb-2021)

Ref Expression
Assertion fvffz0 ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 𝐼 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ) → 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) → 𝐼 ∈ ℕ0 )
3 simp1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) → 𝑁 ∈ ℕ0 )
4 nn0re ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
5 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
6 ltle ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐼 < 𝑁 → 𝐼 ≤ 𝑁 ) )
7 4 5 6 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 < 𝑁 → 𝐼 ≤ 𝑁 ) )
8 7 3impia ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) → 𝐼 ≤ 𝑁 )
9 elfz2nn0 ⊢ ( 𝐼 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ≤ 𝑁 ) )
10 2 3 8 9 syl3anbrc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) → 𝐼 ∈ ( 0 ... 𝑁 ) )
11 10 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ) → 𝐼 ∈ ( 0 ... 𝑁 ) )
12 1 11 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < 𝑁 ) ∧ 𝑃 : ( 0 ... 𝑁 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 𝐼 ) ∈ 𝑉 )