This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mptnn0fsuppd

Description: A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 2-Dec-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 )
mptnn0fsuppd.d 
|- ( k = x -> C = D )
mptnn0fsuppd.s 
|- ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> D = .0. ) )
Assertion mptnn0fsuppd 
|- ( ph -> ( k e. NN0 |-> C ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 mptnn0fsupp.0 
 |-  ( ph -> .0. e. V )
2 mptnn0fsupp.c 
 |-  ( ( ph /\ k e. NN0 ) -> C e. B )
3 mptnn0fsuppd.d 
 |-  ( k = x -> C = D )
4 mptnn0fsuppd.s 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> D = .0. ) )
5 vex 
 |-  x e. _V
6 5 3 csbie 
 |-  [_ x / k ]_ C = D
7 id 
 |-  ( D = .0. -> D = .0. )
8 6 7 eqtrid 
 |-  ( D = .0. -> [_ x / k ]_ C = .0. )
9 8 imim2i 
 |-  ( ( s < x -> D = .0. ) -> ( s < x -> [_ x / k ]_ C = .0. ) )
10 9 ralimi 
 |-  ( A. x e. NN0 ( s < x -> D = .0. ) -> A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
11 10 reximi 
 |-  ( E. s e. NN0 A. x e. NN0 ( s < x -> D = .0. ) -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
12 4 11 syl 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
13 1 2 12 mptnn0fsupp 
 |-  ( ph -> ( k e. NN0 |-> C ) finSupp .0. )