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