Metamath Proof Explorer

Theorem fsuppxpfi

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

Ref Expression
Assertion fsuppxpfi ⊢ finSupp Z⁡ F ∧ finSupp Z⁡ G → supp Z⁡ F × supp Z⁡ G ∈ Fin

Proof

Step Hyp Ref Expression
1 id ⊢ finSupp Z⁡ F → finSupp Z⁡ F
2 1 fsuppimpd ⊢ finSupp Z⁡ F → F supp Z ∈ Fin
3 id ⊢ finSupp Z⁡ G → finSupp Z⁡ G
4 3 fsuppimpd ⊢ finSupp Z⁡ G → G supp Z ∈ Fin
5 xpfi ⊢ F supp Z ∈ Fin ∧ G supp Z ∈ Fin → supp Z⁡ F × supp Z⁡ G ∈ Fin
6 2 4 5 syl2an ⊢ finSupp Z⁡ F ∧ finSupp Z⁡ G → supp Z⁡ F × supp Z⁡ G ∈ Fin