Theorem fczfsuppd

Description: A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019)

	Ref	Expression
Hypotheses	fczfsuppd.b	$$⊢\phi \to B\in V$$
	fczfsuppd.z	$$⊢\phi \to Z\in W$$
Assertion	fczfsuppd	$$⊢\phi \to {finSupp}_Z\left(\left(B\times \left\{Z\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fczfsuppd.b	$$⊢\phi \to B\in V$$
2		fczfsuppd.z	$$⊢\phi \to Z\in W$$
3		snex	$$⊢\left\{Z\right\}\in \mathrm{V}$$
4		xpexg	$$⊢\left(B\in V\wedge \left\{Z\right\}\in \mathrm{V}\right)\to B\times \left\{Z\right\}\in \mathrm{V}$$
5	1 3 4	sylancl	$$⊢\phi \to B\times \left\{Z\right\}\in \mathrm{V}$$
6		fnconstg	$$⊢Z\in W\to \left(B\times \left\{Z\right\}\right)FnB$$
7		fnfun	$$⊢\left(B\times \left\{Z\right\}\right)FnB\to \mathrm{Fun}\left(B\times \left\{Z\right\}\right)$$
8	2 6 7	3syl	$$⊢\phi \to \mathrm{Fun}\left(B\times \left\{Z\right\}\right)$$
9		fczsupp0	$$⊢\left(B\times \left\{Z\right\}\right)\mathrm{supp}Z=\varnothing$$
10		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
11	9 10	eqeltri	$$⊢\left(B\times \left\{Z\right\}\right)\mathrm{supp}Z\in \mathrm{Fin}$$
12	11	a1i	$$⊢\phi \to \left(B\times \left\{Z\right\}\right)\mathrm{supp}Z\in \mathrm{Fin}$$
13	5 2 8 12	isfsuppd	$$⊢\phi \to {finSupp}_Z\left(\left(B\times \left\{Z\right\}\right)\right)$$