Theorem fsuppxpfi

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

	Ref	Expression
Assertion	fsuppxpfi	⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( ( 𝐹 supp 𝑍 ) × ( 𝐺 supp 𝑍 ) ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 finSupp 𝑍 → 𝐹 finSupp 𝑍 )
2	1	fsuppimpd	⊢ ( 𝐹 finSupp 𝑍 → ( 𝐹 supp 𝑍 ) ∈ Fin )
3		id	⊢ ( 𝐺 finSupp 𝑍 → 𝐺 finSupp 𝑍 )
4	3	fsuppimpd	⊢ ( 𝐺 finSupp 𝑍 → ( 𝐺 supp 𝑍 ) ∈ Fin )
5		xpfi	⊢ ( ( ( 𝐹 supp 𝑍 ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ∈ Fin ) → ( ( 𝐹 supp 𝑍 ) × ( 𝐺 supp 𝑍 ) ) ∈ Fin )
6	2 4 5	syl2an	⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( ( 𝐹 supp 𝑍 ) × ( 𝐺 supp 𝑍 ) ) ∈ Fin )