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	|- ( ( ( N e. NN0 /\ I e. NN0 /\ I < N ) /\ P : ( 0 ... N ) --> V ) -> ( P ` I ) e. V )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( ( N e. NN0 /\ I e. NN0 /\ I < N ) /\ P : ( 0 ... N ) --> V ) -> P : ( 0 ... N ) --> V )
2		simp2	|- ( ( N e. NN0 /\ I e. NN0 /\ I < N ) -> I e. NN0 )
3		simp1	|- ( ( N e. NN0 /\ I e. NN0 /\ I < N ) -> N e. NN0 )
4		nn0re	|- ( I e. NN0 -> I e. RR )
5		nn0re	|- ( N e. NN0 -> N e. RR )
6		ltle	|- ( ( I e. RR /\ N e. RR ) -> ( I < N -> I <_ N ) )
7	4 5 6	syl2anr	|- ( ( N e. NN0 /\ I e. NN0 ) -> ( I < N -> I <_ N ) )
8	7	3impia	|- ( ( N e. NN0 /\ I e. NN0 /\ I < N ) -> I <_ N )
9		elfz2nn0	|- ( I e. ( 0 ... N ) <-> ( I e. NN0 /\ N e. NN0 /\ I <_ N ) )
10	2 3 8 9	syl3anbrc	|- ( ( N e. NN0 /\ I e. NN0 /\ I < N ) -> I e. ( 0 ... N ) )
11	10	adantr	|- ( ( ( N e. NN0 /\ I e. NN0 /\ I < N ) /\ P : ( 0 ... N ) --> V ) -> I e. ( 0 ... N ) )
12	1 11	ffvelcdmd	|- ( ( ( N e. NN0 /\ I e. NN0 /\ I < N ) /\ P : ( 0 ... N ) --> V ) -> ( P ` I ) e. V )