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 
|- ( ( ( 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 )