Metamath Proof Explorer

Theorem mptnn0fsuppr

Description: A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-2019) (Revised by AV, 23-Dec-2019)

Ref Expression
Hypotheses mptnn0fsupp.0 
|- ( ph -> .0. e. V )
mptnn0fsupp.c 
|- ( ( ph /\ k e. NN0 ) -> C e. B )
mptnn0fsuppr.s 
|- ( ph -> ( k e. NN0 |-> C ) finSupp .0. )
Assertion mptnn0fsuppr 
|- ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )

Proof

Step Hyp Ref Expression
1 mptnn0fsupp.0 
 |-  ( ph -> .0. e. V )
2 mptnn0fsupp.c 
 |-  ( ( ph /\ k e. NN0 ) -> C e. B )
3 mptnn0fsuppr.s 
 |-  ( ph -> ( k e. NN0 |-> C ) finSupp .0. )
4 fsuppimp 
 |-  ( ( k e. NN0 |-> C ) finSupp .0. -> ( Fun ( k e. NN0 |-> C ) /\ ( ( k e. NN0 |-> C ) supp .0. ) e. Fin ) )
5 2 ralrimiva 
 |-  ( ph -> A. k e. NN0 C e. B )
6 eqid 
 |-  ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
7 6 fnmpt 
 |-  ( A. k e. NN0 C e. B -> ( k e. NN0 |-> C ) Fn NN0 )
8 5 7 syl 
 |-  ( ph -> ( k e. NN0 |-> C ) Fn NN0 )
9 nn0ex 
 |-  NN0 e. _V
10 9 a1i 
 |-  ( ph -> NN0 e. _V )
11 1 elexd 
 |-  ( ph -> .0. e. _V )
12 8 10 11 3jca 
 |-  ( ph -> ( ( k e. NN0 |-> C ) Fn NN0 /\ NN0 e. _V /\ .0. e. _V ) )
13 12 adantr 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> ( ( k e. NN0 |-> C ) Fn NN0 /\ NN0 e. _V /\ .0. e. _V ) )
14 suppvalfn 
 |-  ( ( ( k e. NN0 |-> C ) Fn NN0 /\ NN0 e. _V /\ .0. e. _V ) -> ( ( k e. NN0 |-> C ) supp .0. ) = { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } )
15 13 14 syl 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> ( ( k e. NN0 |-> C ) supp .0. ) = { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } )
16 simpr 
 |-  ( ( ( ph /\ Fun ( k e. NN0 |-> C ) ) /\ x e. NN0 ) -> x e. NN0 )
17 5 adantr 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> A. k e. NN0 C e. B )
18 17 adantr 
 |-  ( ( ( ph /\ Fun ( k e. NN0 |-> C ) ) /\ x e. NN0 ) -> A. k e. NN0 C e. B )
19 rspcsbela 
 |-  ( ( x e. NN0 /\ A. k e. NN0 C e. B ) -> [_ x / k ]_ C e. B )
20 16 18 19 syl2anc 
 |-  ( ( ( ph /\ Fun ( k e. NN0 |-> C ) ) /\ x e. NN0 ) -> [_ x / k ]_ C e. B )
21 6 fvmpts 
 |-  ( ( x e. NN0 /\ [_ x / k ]_ C e. B ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
22 16 20 21 syl2anc 
 |-  ( ( ( ph /\ Fun ( k e. NN0 |-> C ) ) /\ x e. NN0 ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
23 22 neeq1d 
 |-  ( ( ( ph /\ Fun ( k e. NN0 |-> C ) ) /\ x e. NN0 ) -> ( ( ( k e. NN0 |-> C ) ` x ) =/= .0. <-> [_ x / k ]_ C =/= .0. ) )
24 23 rabbidva 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } = { x e. NN0 | [_ x / k ]_ C =/= .0. } )
25 15 24 eqtrd 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> ( ( k e. NN0 |-> C ) supp .0. ) = { x e. NN0 | [_ x / k ]_ C =/= .0. } )
26 25 eleq1d 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> ( ( ( k e. NN0 |-> C ) supp .0. ) e. Fin <-> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) )
27 26 biimpd 
 |-  ( ( ph /\ Fun ( k e. NN0 |-> C ) ) -> ( ( ( k e. NN0 |-> C ) supp .0. ) e. Fin -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) )
28 27 expcom 
 |-  ( Fun ( k e. NN0 |-> C ) -> ( ph -> ( ( ( k e. NN0 |-> C ) supp .0. ) e. Fin -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) ) )
29 28 com23 
 |-  ( Fun ( k e. NN0 |-> C ) -> ( ( ( k e. NN0 |-> C ) supp .0. ) e. Fin -> ( ph -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) ) )
30 29 imp 
 |-  ( ( Fun ( k e. NN0 |-> C ) /\ ( ( k e. NN0 |-> C ) supp .0. ) e. Fin ) -> ( ph -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) )
31 4 30 syl 
 |-  ( ( k e. NN0 |-> C ) finSupp .0. -> ( ph -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin ) )
32 3 31 mpcom 
 |-  ( ph -> { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin )
33 rabssnn0fi 
 |-  ( { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. [_ x / k ]_ C =/= .0. ) )
34 nne 
 |-  ( -. [_ x / k ]_ C =/= .0. <-> [_ x / k ]_ C = .0. )
35 34 imbi2i 
 |-  ( ( s < x -> -. [_ x / k ]_ C =/= .0. ) <-> ( s < x -> [_ x / k ]_ C = .0. ) )
36 35 ralbii 
 |-  ( A. x e. NN0 ( s < x -> -. [_ x / k ]_ C =/= .0. ) <-> A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
37 36 rexbii 
 |-  ( E. s e. NN0 A. x e. NN0 ( s < x -> -. [_ x / k ]_ C =/= .0. ) <-> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
38 33 37 bitri 
 |-  ( { x e. NN0 | [_ x / k ]_ C =/= .0. } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
39 32 38 sylib 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )