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

Metamath Proof Explorer

Theorem fsuppmptdm

Description: A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019)

Ref Expression
Hypotheses fsuppmptdm.f ⊢ F = x ∈ A ⟼ Y
fsuppmptdm.a ⊢ φ → A ∈ Fin
fsuppmptdm.y ⊢ φ ∧ x ∈ A → Y ∈ V
fsuppmptdm.z ⊢ φ → Z ∈ W
Assertion fsuppmptdm ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 fsuppmptdm.f ⊢ F = x ∈ A ⟼ Y
2 fsuppmptdm.a ⊢ φ → A ∈ Fin
3 fsuppmptdm.y ⊢ φ ∧ x ∈ A → Y ∈ V
4 fsuppmptdm.z ⊢ φ → Z ∈ W
5 3 1 fmptd ⊢ φ → F : A ⟶ V
6 5 2 4 fdmfifsupp ⊢ φ → finSupp Z⁡ F