Theorem 0fsupp

Description: The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019)

	Ref	Expression
Assertion	0fsupp	$$⊢Z\in V\to {finSupp}_Z\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		supp0	$$⊢Z\in V\to \varnothing \mathrm{supp}Z=\varnothing$$
2		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
3	1 2	eqeltrdi	$$⊢Z\in V\to \varnothing \mathrm{supp}Z\in \mathrm{Fin}$$
4		fun0	$$⊢\mathrm{Fun}\varnothing$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6		funisfsupp	$$⊢\left(\mathrm{Fun}\varnothing \wedge \varnothing \in \mathrm{V}\wedge Z\in V\right)\to \left({finSupp}_Z\left(\varnothing \right)\leftrightarrow \varnothing \mathrm{supp}Z\in \mathrm{Fin}\right)$$
7	4 5 6	mp3an12	$$⊢Z\in V\to \left({finSupp}_Z\left(\varnothing \right)\leftrightarrow \varnothing \mathrm{supp}Z\in \mathrm{Fin}\right)$$
8	3 7	mpbird	$$⊢Z\in V\to {finSupp}_Z\left(\varnothing \right)$$