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

Metamath Proof Explorer

Theorem fidmfisupp

Description: A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fidmfisupp.1 ⊢ φ → F : D ⟶ R
fidmfisupp.2 ⊢ φ → D ∈ Fin
fidmfisupp.3 ⊢ φ → Z ∈ V
Assertion fidmfisupp ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 fidmfisupp.1 ⊢ φ → F : D ⟶ R
2 fidmfisupp.2 ⊢ φ → D ∈ Fin
3 fidmfisupp.3 ⊢ φ → Z ∈ V
4 1 2 fexd ⊢ φ → F ∈ V
5 suppimacnv ⊢ F ∈ V ∧ Z ∈ V → F supp Z = F -1 V ∖ Z
6 4 3 5 syl2anc ⊢ φ → F supp Z = F -1 V ∖ Z
7 2 1 fisuppfi ⊢ φ → F -1 V ∖ Z ∈ Fin
8 6 7 eqeltrd ⊢ φ → F supp Z ∈ Fin
9 1 ffund ⊢ φ → Fun ⁡ F
10 funisfsupp ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ V → finSupp Z⁡ F ↔ F supp Z ∈ Fin
11 9 4 3 10 syl3anc ⊢ φ → finSupp Z⁡ F ↔ F supp Z ∈ Fin
12 8 11 mpbird ⊢ φ → finSupp Z⁡ F