Metamath Proof Explorer


Theorem fsuppmptif

Description: A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019)

Ref Expression
Hypotheses fsuppmptif.f φ F : A B
fsuppmptif.a φ A V
fsuppmptif.z φ Z W
fsuppmptif.s φ finSupp Z F
Assertion fsuppmptif φ finSupp Z k A if k D F k Z

Proof

Step Hyp Ref Expression
1 fsuppmptif.f φ F : A B
2 fsuppmptif.a φ A V
3 fsuppmptif.z φ Z W
4 fsuppmptif.s φ finSupp Z F
5 fvex F k V
6 3 adantr φ k A Z W
7 ifexg F k V Z W if k D F k Z V
8 5 6 7 sylancr φ k A if k D F k Z V
9 8 fmpttd φ k A if k D F k Z : A V
10 9 ffund φ Fun k A if k D F k Z
11 4 fsuppimpd φ F supp Z Fin
12 ssidd φ F supp Z F supp Z
13 1 12 2 3 suppssr φ k A supp Z F F k = Z
14 13 ifeq1d φ k A supp Z F if k D F k Z = if k D Z Z
15 ifid if k D Z Z = Z
16 14 15 eqtrdi φ k A supp Z F if k D F k Z = Z
17 16 2 suppss2 φ k A if k D F k Z supp Z F supp Z
18 11 17 ssfid φ k A if k D F k Z supp Z Fin
19 2 mptexd φ k A if k D F k Z V
20 isfsupp k A if k D F k Z V Z W finSupp Z k A if k D F k Z Fun k A if k D F k Z k A if k D F k Z supp Z Fin
21 19 3 20 syl2anc φ finSupp Z k A if k D F k Z Fun k A if k D F k Z k A if k D F k Z supp Z Fin
22 10 18 21 mpbir2and φ finSupp Z k A if k D F k Z