Theorem indfsd

Description: The indicator function of a finite set has finite support. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	indfsd.1	$$⊢\phi \to O\in V$$
	indfsd.2	$$⊢\phi \to A\subseteq O$$
	indfsd.3	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	indfsd	$$⊢\phi \to {finSupp}_0\left({𝟙}_O\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		indfsd.1	$$⊢\phi \to O\in V$$
2		indfsd.2	$$⊢\phi \to A\subseteq O$$
3		indfsd.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		fvexd	$$⊢\phi \to {𝟙}_O\left(A\right)\in \mathrm{V}$$
5		c0ex	$$⊢0\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
7		indf	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right):O⟶\left\{0,1\right\}$$
8	1 2 7	syl2anc	$$⊢\phi \to {𝟙}_O\left(A\right):O⟶\left\{0,1\right\}$$
9	8	ffund	$$⊢\phi \to \mathrm{Fun}{𝟙}_O\left(A\right)$$
10		indsupp	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)\mathrm{supp}0=A$$
11	1 2 10	syl2anc	$$⊢\phi \to {𝟙}_O\left(A\right)\mathrm{supp}0=A$$
12	11 3	eqeltrd	$$⊢\phi \to {𝟙}_O\left(A\right)\mathrm{supp}0\in \mathrm{Fin}$$
13	4 6 9 12	isfsuppd	$$⊢\phi \to {finSupp}_0\left({𝟙}_O\left(A\right)\right)$$