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

Metamath Proof Explorer

Theorem fdmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019)

Ref Expression
Hypotheses fdmfisuppfi.f ⊢ φ → F : D ⟶ R
fdmfisuppfi.d ⊢ φ → D ∈ Fin
fdmfisuppfi.z ⊢ φ → Z ∈ V
Assertion fdmfifsupp ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 fdmfisuppfi.f ⊢ φ → F : D ⟶ R
2 fdmfisuppfi.d ⊢ φ → D ∈ Fin
3 fdmfisuppfi.z ⊢ φ → Z ∈ V
4 1 ffund ⊢ φ → Fun ⁡ F
5 1 2 3 fdmfisuppfi ⊢ φ → F supp Z ∈ Fin
6 1 ffnd ⊢ φ → F Fn D
7 fnex ⊢ F Fn D ∧ D ∈ Fin → F ∈ V
8 6 2 7 syl2anc ⊢ φ → F ∈ V
9 isfsupp ⊢ F ∈ V ∧ Z ∈ V → finSupp Z⁡ F ↔ Fun ⁡ F ∧ F supp Z ∈ Fin
10 8 3 9 syl2anc ⊢ φ → finSupp Z⁡ F ↔ Fun ⁡ F ∧ F supp Z ∈ Fin
11 4 5 10 mpbir2and ⊢ φ → finSupp Z⁡ F