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	|- ( ph -> O e. V )
	indfsd.2	|- ( ph -> A C_ O )
	indfsd.3	|- ( ph -> A e. Fin )
Assertion	indfsd	|- ( ph -> ( ( _Ind ` O ) ` A ) finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		indfsd.1	|- ( ph -> O e. V )
2		indfsd.2	|- ( ph -> A C_ O )
3		indfsd.3	|- ( ph -> A e. Fin )
4		fvexd	|- ( ph -> ( ( _Ind ` O ) ` A ) e. _V )
5		c0ex	|- 0 e. _V
6	5	a1i	|- ( ph -> 0 e. _V )
7		indf	|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
8	1 2 7	syl2anc	|- ( ph -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
9	8	ffund	|- ( ph -> Fun ( ( _Ind ` O ) ` A ) )
10		indsupp	|- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )
11	1 2 10	syl2anc	|- ( ph -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )
12	11 3	eqeltrd	|- ( ph -> ( ( ( _Ind ` O ) ` A ) supp 0 ) e. Fin )
13	4 6 9 12	isfsuppd	|- ( ph -> ( ( _Ind ` O ) ` A ) finSupp 0 )