Theorem mptnn0fsupp

Description: A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 5-Oct-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$$
	mptnn0fsupp.s	$$⊢\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)$$
Assertion	mptnn0fsupp	$$⊢\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		mptnn0fsupp.s	$$⊢\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)$$
4	2	ralrimiva	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}C\in B$$
5		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼C\right)=\left(k\in {\mathbb{N}}_0⟼C\right)$$
6	5	fnmpt	$$⊢\forall k\in {\mathbb{N}}_{0}C\in B\to \left(k\in {\mathbb{N}}_0⟼C\right)Fn{\mathbb{N}}_0$$
7	4 6	syl	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right)Fn{\mathbb{N}}_0$$
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
10	1	elexd	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
11		suppvalfn	$$⊢\left(\left(k\in {\mathbb{N}}_0⟼C\right)Fn{\mathbb{N}}_0\wedge {\mathbb{N}}_0\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in {\mathbb{N}}_0|\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
12	7 9 10 11	syl3anc	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in {\mathbb{N}}_0|\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
13		nne	$$⊢\neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}$$
14		simpr	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to x\in {\mathbb{N}}_0$$
15	4	ad2antrr	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to \forall k\in {\mathbb{N}}_{0}C\in B$$
16		rspcsbela	$$⊢\left(x\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋x/k⦌C\in B$$
17	14 15 16	syl2anc	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to ⦋x/k⦌C\in B$$
18	5	fvmpts	$$⊢\left(x\in {\mathbb{N}}_0\wedge ⦋x/k⦌C\in B\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=⦋x/k⦌C$$
19	14 17 18	syl2anc	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=⦋x/k⦌C$$
20	19	eqeq1d	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=\underset{\dot{}}{0}\leftrightarrow ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
21	13 20	syl5bb	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(\neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
22	21	imbi2d	$$⊢\left(\left(\phi \wedge s\in {\mathbb{N}}_0\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(\left(s<x\to \neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\right)$$
23	22	ralbidva	$$⊢\left(\phi \wedge s\in {\mathbb{N}}_0\right)\to \left(\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\right)$$
24	23	rexbidva	$$⊢\phi \to \left(\exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right)\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)\right)$$
25	3 24	mpbird	$$⊢\phi \to \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right)$$
26		rabssnn0fi	$$⊢\left\{x\in {\mathbb{N}}_0|\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right)$$
27	25 26	sylibr	$$⊢\phi \to \left\{x\in {\mathbb{N}}_0|\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
28	12 27	eqeltrd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
29		funmpt	$$⊢\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)$$
30	8	mptex	$$⊢\left(k\in {\mathbb{N}}_0⟼C\right)\in \mathrm{V}$$
31		funisfsupp	$$⊢\left(\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\wedge \left(k\in {\mathbb{N}}_0⟼C\right)\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
32	29 30 10 31	mp3an12i	$$⊢\phi \to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)\leftrightarrow \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
33	28 32	mpbird	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)$$