Theorem fsuppxpfi

Description: The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019)

	Ref	Expression
Assertion	fsuppxpfi	|- ( ( F finSupp Z /\ G finSupp Z ) -> ( ( F supp Z ) X. ( G supp Z ) ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( F finSupp Z -> F finSupp Z )
2	1	fsuppimpd	|- ( F finSupp Z -> ( F supp Z ) e. Fin )
3		id	|- ( G finSupp Z -> G finSupp Z )
4	3	fsuppimpd	|- ( G finSupp Z -> ( G supp Z ) e. Fin )
5		xpfi	|- ( ( ( F supp Z ) e. Fin /\ ( G supp Z ) e. Fin ) -> ( ( F supp Z ) X. ( G supp Z ) ) e. Fin )
6	2 4 5	syl2an	|- ( ( F finSupp Z /\ G finSupp Z ) -> ( ( F supp Z ) X. ( G supp Z ) ) e. Fin )