Theorem fsuppmapnn0ub

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for the arguments resulting in nonzero values. (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Assertion	fsuppmapnn0ub	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\to \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\wedge {finSupp}_Z\left(F\right)\right)\to {finSupp}_Z\left(F\right)$$
2	1	fsuppimpd	$$⊢\left(\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\wedge {finSupp}_Z\left(F\right)\right)\to F\mathrm{supp}Z\in \mathrm{Fin}$$
3	2	ex	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\to F\mathrm{supp}Z\in \mathrm{Fin}\right)$$
4		elmapfn	$$⊢F\in \left(R^{{\mathbb{N}}_0}\right)\to FFn{\mathbb{N}}_0$$
5	4	adantr	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to FFn{\mathbb{N}}_0$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7	6	a1i	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
8		simpr	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to Z\in V$$
9		suppvalfn	$$⊢\left(FFn{\mathbb{N}}_0\wedge {\mathbb{N}}_0\in \mathrm{V}\wedge Z\in V\right)\to F\mathrm{supp}Z=\left\{x\in {\mathbb{N}}_0|F\left(x\right)\ne Z\right\}$$
10	5 7 8 9	syl3anc	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to F\mathrm{supp}Z=\left\{x\in {\mathbb{N}}_0|F\left(x\right)\ne Z\right\}$$
11	10	eleq1d	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to \left(F\mathrm{supp}Z\in \mathrm{Fin}\leftrightarrow \left\{x\in {\mathbb{N}}_0|F\left(x\right)\ne Z\right\}\in \mathrm{Fin}\right)$$
12		rabssnn0fi	$$⊢\left\{x\in {\mathbb{N}}_0|F\left(x\right)\ne Z\right\}\in \mathrm{Fin}\leftrightarrow \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to \neg F\left(x\right)\ne Z\right)$$
13		nne	$$⊢\neg F\left(x\right)\ne Z\leftrightarrow F\left(x\right)=Z$$
14	13	imbi2i	$$⊢\left(m<x\to \neg F\left(x\right)\ne Z\right)\leftrightarrow \left(m<x\to F\left(x\right)=Z\right)$$
15	14	ralbii	$$⊢\forall x\in {\mathbb{N}}_0\left(m<x\to \neg F\left(x\right)\ne Z\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)$$
16	15	rexbii	$$⊢\exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to \neg F\left(x\right)\ne Z\right)\leftrightarrow \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)$$
17	12 16	sylbb	$$⊢\left\{x\in {\mathbb{N}}_0|F\left(x\right)\ne Z\right\}\in \mathrm{Fin}\to \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)$$
18	11 17	syl6bi	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to \left(F\mathrm{supp}Z\in \mathrm{Fin}\to \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)\right)$$
19	3 18	syld	$$⊢\left(F\in \left(R^{{\mathbb{N}}_0}\right)\wedge Z\in V\right)\to \left({finSupp}_Z\left(F\right)\to \exists m\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(m<x\to F\left(x\right)=Z\right)\right)$$