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	|- ( ph -> F finSupp Z )
	fsuppun.g	|- ( ph -> G finSupp Z )
Assertion	fsuppunfi	|- ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppun.f	|- ( ph -> F finSupp Z )
2		fsuppun.g	|- ( ph -> G finSupp Z )
3		fsuppimp	|- ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
4		fsuppimp	|- ( G finSupp Z -> ( Fun G /\ ( G supp Z ) e. Fin ) )
5		unfi	|- ( ( ( F supp Z ) e. Fin /\ ( G supp Z ) e. Fin ) -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin )
6	5	expcom	|- ( ( G supp Z ) e. Fin -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) )
7	6	adantl	|- ( ( Fun G /\ ( G supp Z ) e. Fin ) -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) )
8	2 4 7	3syl	|- ( ph -> ( ( F supp Z ) e. Fin -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) )
9	8	com12	|- ( ( F supp Z ) e. Fin -> ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) )
10	3 9	simpl2im	|- ( F finSupp Z -> ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin ) )
11	1 10	mpcom	|- ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) e. Fin )