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 ⊢ φ → O ∈ V
indfsd.2 ⊢ φ → A ⊆ O
indfsd.3 ⊢ φ → A ∈ Fin
Assertion indfsd ⊢ φ → finSupp 0 ⁡ 𝟙 O ⁡ A

Proof

Step Hyp Ref Expression
1 indfsd.1 ⊢ φ → O ∈ V
2 indfsd.2 ⊢ φ → A ⊆ O
3 indfsd.3 ⊢ φ → A ∈ Fin
4 fvexd ⊢ φ → 𝟙 O ⁡ A ∈ V
5 c0ex ⊢ 0 ∈ V
6 5 a1i ⊢ φ → 0 ∈ V
7 indf ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A : O ⟶ 0 1
8 1 2 7 syl2anc ⊢ φ → 𝟙 O ⁡ A : O ⟶ 0 1
9 8 ffund ⊢ φ → Fun ⁡ 𝟙 O ⁡ A
10 indsupp ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A supp 0 = A
11 1 2 10 syl2anc ⊢ φ → 𝟙 O ⁡ A supp 0 = A
12 11 3 eqeltrd ⊢ φ → 𝟙 O ⁡ A supp 0 ∈ Fin
13 4 6 9 12 isfsuppd ⊢ φ → finSupp 0 ⁡ 𝟙 O ⁡ A