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

Metamath Proof Explorer

Theorem fdmfisuppfi

Description: The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 fdmfisuppfi.f ⊢ φ → F : D ⟶ R
2 fdmfisuppfi.d ⊢ φ → D ∈ Fin
3 fdmfisuppfi.z ⊢ φ → 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