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