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 ... 𝑁 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 𝐼 ) ∈ 𝑉 )