Metamath Proof Explorer


Theorem fsuppunfi

Description: The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019)

Ref Expression
Hypotheses fsuppun.f φ finSupp Z F
fsuppun.g φ finSupp Z G
Assertion fsuppunfi φ supp Z F supp Z G Fin

Proof

Step Hyp Ref Expression
1 fsuppun.f φ finSupp Z F
2 fsuppun.g φ finSupp Z G
3 fsuppimp finSupp Z F Fun F F supp Z Fin
4 fsuppimp finSupp Z G Fun G G supp Z Fin
5 unfi F supp Z Fin G supp Z Fin supp Z F supp Z G Fin
6 5 expcom G supp Z Fin F supp Z Fin supp Z F supp Z G Fin
7 6 adantl Fun G G supp Z Fin F supp Z Fin supp Z F supp Z G Fin
8 2 4 7 3syl φ F supp Z Fin supp Z F supp Z G Fin
9 8 com12 F supp Z Fin φ supp Z F supp Z G Fin
10 3 9 simpl2im finSupp Z F φ supp Z F supp Z G Fin
11 1 10 mpcom φ supp Z F supp Z G Fin