This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )