Metamath Proof Explorer

Theorem fsuppmapnn0fz

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019) (Proof shortened by AV, 6-Oct-2019)

Ref Expression
Assertion fsuppmapnn0fz 
|- ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0ub 
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) )
2 simpllr 
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> Z e. V )
3 simplll 
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> F e. ( R ^m NN0 ) )
4 simplr 
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> m e. NN0 )
5 simpr 
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> A. x e. NN0 ( m < x -> ( F ` x ) = Z ) )
6 2 3 4 5 suppssfz 
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> ( F supp Z ) C_ ( 0 ... m ) )
7 6 ex 
 |-  ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) -> ( A. x e. NN0 ( m < x -> ( F ` x ) = Z ) -> ( F supp Z ) C_ ( 0 ... m ) ) )
8 7 reximdva 
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( E. m e. NN0 A. x e. NN0 ( m < x -> ( F ` x ) = Z ) -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )
9 1 8 syld 
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )