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

Metamath Proof Explorer

Theorem fndmfifsupp

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

Ref Expression
Hypotheses fndmfisuppfi.f ⊢ φ → F Fn D
fndmfisuppfi.d ⊢ φ → D ∈ Fin
fndmfisuppfi.z ⊢ φ → Z ∈ V
Assertion fndmfifsupp ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 fndmfisuppfi.f ⊢ φ → F Fn D
2 fndmfisuppfi.d ⊢ φ → D ∈ Fin
3 fndmfisuppfi.z ⊢ φ → Z ∈ V
4 dffn3 ⊢ F Fn D ↔ F : D ⟶ ran ⁡ F
5 1 4 sylib ⊢ φ → F : D ⟶ ran ⁡ F
6 5 2 3 fdmfifsupp ⊢ φ → finSupp Z⁡ F