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 φfinSuppZF
fsuppun.g φfinSuppZG
Assertion fsuppunfi φsuppZFsuppZGFin

Proof

Step Hyp Ref Expression
1 fsuppun.f φfinSuppZF
2 fsuppun.g φfinSuppZG
3 fsuppimp finSuppZFFunFFsuppZFin
4 fsuppimp finSuppZGFunGGsuppZFin
5 unfi FsuppZFinGsuppZFinsuppZFsuppZGFin
6 5 expcom GsuppZFinFsuppZFinsuppZFsuppZGFin
7 6 adantl FunGGsuppZFinFsuppZFinsuppZFsuppZGFin
8 2 4 7 3syl φFsuppZFinsuppZFsuppZGFin
9 8 com12 FsuppZFinφsuppZFsuppZGFin
10 3 9 simpl2im finSuppZFφsuppZFsuppZGFin
11 1 10 mpcom φsuppZFsuppZGFin