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	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	indfsd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
	indfsd.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion	indfsd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		indfsd.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		indfsd.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
3		indfsd.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fvexd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ∈ V )
5		c0ex	⊢ 0 ∈ V
6	5	a1i	⊢ ( 𝜑 → 0 ∈ V )
7		indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
9	8	ffund	⊢ ( 𝜑 → Fun ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) )
10		indsupp	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )
11	1 2 10	syl2anc	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )
12	11 3	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) ∈ Fin )
13	4 6 9 12	isfsuppd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) finSupp 0 )