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	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
	mptnn0fsupp.c	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to C\in B$$
	mptnn0fsuppd.d	$$⊢k=x\to C=D$$
	mptnn0fsuppd.s	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to D=\underset{\dot{}}{0}\right)$$
Assertion	mptnn0fsuppd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptnn0fsupp.0	$$⊢\phi \to \underset{\dot{}}{0}\in V$$
2		mptnn0fsupp.c	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to C\in B$$
3		mptnn0fsuppd.d	$$⊢k=x\to C=D$$
4		mptnn0fsuppd.s	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to D=\underset{\dot{}}{0}\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5 3	csbie	$$⊢⦋x/k⦌C=D$$
7		id	$$⊢D=\underset{\dot{}}{0}\to D=\underset{\dot{}}{0}$$
8	6 7	syl5eq	$$⊢D=\underset{\dot{}}{0}\to ⦋x/k⦌C=\underset{\dot{}}{0}$$
9	8	imim2i	$$⊢\left(s<x\to D=\underset{\dot{}}{0}\right)\to \left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
10	9	ralimi	$$⊢\forall x\in {\mathbb{N}}_0\left(s<x\to D=\underset{\dot{}}{0}\right)\to \forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
11	10	reximi	$$⊢\exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to D=\underset{\dot{}}{0}\right)\to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
12	4 11	syl	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
13	1 2 12	mptnn0fsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)$$