Theorem mptnn0fsuppr

Description: A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-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$$
	mptnn0fsuppr.s	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)$$
Assertion	mptnn0fsuppr	$$⊢\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)$$

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		mptnn0fsuppr.s	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)$$
4		fsuppimp	$$⊢{finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left(\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\wedge \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
5	2	ralrimiva	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}C\in B$$
6		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼C\right)=\left(k\in {\mathbb{N}}_0⟼C\right)$$
7	6	fnmpt	$$⊢\forall k\in {\mathbb{N}}_{0}C\in B\to \left(k\in {\mathbb{N}}_0⟼C\right)Fn{\mathbb{N}}_0$$
8	5 7	syl	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼C\right)Fn{\mathbb{N}}_0$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
11	1	elexd	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
12	8 10 11	3jca	$$⊢\phi \to \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)$$
13	12	adantr	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \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)$$
14		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\}$$
15	13 14	syl	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\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\}$$
16		simpr	$$⊢\left(\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to x\in {\mathbb{N}}_0$$
17	5	adantr	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \forall k\in {\mathbb{N}}_{0}C\in B$$
18	17	adantr	$$⊢\left(\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to \forall k\in {\mathbb{N}}_{0}C\in B$$
19		rspcsbela	$$⊢\left(x\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}C\in B\right)\to ⦋x/k⦌C\in B$$
20	16 18 19	syl2anc	$$⊢\left(\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to ⦋x/k⦌C\in B$$
21	6	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$$
22	16 20 21	syl2anc	$$⊢\left(\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)=⦋x/k⦌C$$
23	22	neeq1d	$$⊢\left(\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow ⦋x/k⦌C\ne \underset{\dot{}}{0}\right)$$
24	23	rabbidva	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left\{x\in {\mathbb{N}}_0|\left(k\in {\mathbb{N}}_0⟼C\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}=\left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}$$
25	15 24	eqtrd	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}$$
26	25	eleq1d	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\leftrightarrow \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)$$
27	26	biimpd	$$⊢\left(\phi \wedge \mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)$$
28	27	expcom	$$⊢\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\to \left(\phi \to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)\right)$$
29	28	com23	$$⊢\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\to \left(\left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\to \left(\phi \to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)\right)$$
30	29	imp	$$⊢\left(\mathrm{Fun}\left(k\in {\mathbb{N}}_0⟼C\right)\wedge \left(k\in {\mathbb{N}}_0⟼C\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)\to \left(\phi \to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)$$
31	4 30	syl	$$⊢{finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼C\right)\right)\to \left(\phi \to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}\right)$$
32	3 31	mpcom	$$⊢\phi \to \left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\ne \underset{\dot{}}{0}\right\}\in \mathrm{Fin}$$
33		rabssnn0fi	$$⊢\left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\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 ⦋x/k⦌C\ne \underset{\dot{}}{0}\right)$$
34		nne	$$⊢\neg ⦋x/k⦌C\ne \underset{\dot{}}{0}\leftrightarrow ⦋x/k⦌C=\underset{\dot{}}{0}$$
35	34	imbi2i	$$⊢\left(s<x\to \neg ⦋x/k⦌C\ne \underset{\dot{}}{0}\right)\leftrightarrow \left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
36	35	ralbii	$$⊢\forall x\in {\mathbb{N}}_0\left(s<x\to \neg ⦋x/k⦌C\ne \underset{\dot{}}{0}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(s<x\to ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
37	36	rexbii	$$⊢\exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg ⦋x/k⦌C\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)$$
38	33 37	bitri	$$⊢\left\{x\in {\mathbb{N}}_0|⦋x/k⦌C\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 ⦋x/k⦌C=\underset{\dot{}}{0}\right)$$
39	32 38	sylib	$$⊢\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)$$