Theorem sniffsupp

Description: A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	sniffsupp.i	$$⊢\phi \to I\in V$$
	sniffsupp.0	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
	sniffsupp.f	$$⊢F=\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)$$
Assertion	sniffsupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		sniffsupp.i	$$⊢\phi \to I\in V$$
2		sniffsupp.0	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
3		sniffsupp.f	$$⊢F=\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)$$
4		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
5		eldifsni	$$⊢x\in \left(I\setminus \left\{X\right\}\right)\to x\ne X$$
6	5	adantl	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{X\right\}\right)\right)\to x\ne X$$
7	6	neneqd	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{X\right\}\right)\right)\to \neg x=X$$
8	7	iffalsed	$$⊢\left(\phi \wedge x\in \left(I\setminus \left\{X\right\}\right)\right)\to if\left(x=X,A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
9	8 1	suppss2	$$⊢\phi \to \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
10		ssfi	$$⊢\left(\left\{X\right\}\in \mathrm{Fin}\wedge \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}\right)\to \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
11	4 9 10	sylancr	$$⊢\phi \to \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}$$
12		funmpt	$$⊢\mathrm{Fun}\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)$$
13	1	mptexd	$$⊢\phi \to \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\in \mathrm{V}$$
14		funisfsupp	$$⊢\left(\mathrm{Fun}\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\wedge \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\in \mathrm{V}\wedge \underset{\dot{}}{0}\in W\right)\to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
15	12 13 2 14	mp3an2i	$$⊢\phi \to \left({finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\right)\leftrightarrow \left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\in \mathrm{Fin}\right)$$
16	11 15	mpbird	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in I⟼if\left(x=X,A,\underset{\dot{}}{0}\right)\right)\right)$$
17	3 16	eqbrtrid	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$