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 ⊢ φ → finSupp Z⁡ F
fsuppun.g ⊢ φ → finSupp Z⁡ G
Assertion fsuppunfi ⊢ φ → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin

Proof

Step Hyp Ref Expression
1 fsuppun.f ⊢ φ → finSupp Z⁡ F
2 fsuppun.g ⊢ φ → finSupp Z⁡ G
3 fsuppimp ⊢ finSupp Z⁡ F → Fun ⁡ F ∧ F supp Z ∈ Fin
4 fsuppimp ⊢ finSupp Z⁡ G → Fun ⁡ G ∧ G supp Z ∈ Fin
5 unfi ⊢ F supp Z ∈ Fin ∧ G supp Z ∈ Fin → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
6 5 expcom ⊢ G supp Z ∈ Fin → F supp Z ∈ Fin → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
7 6 adantl ⊢ Fun ⁡ G ∧ G supp Z ∈ Fin → F supp Z ∈ Fin → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
8 2 4 7 3syl ⊢ φ → F supp Z ∈ Fin → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
9 8 com12 ⊢ F supp Z ∈ Fin → φ → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
10 3 9 simpl2im ⊢ finSupp Z⁡ F → φ → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin
11 1 10 mpcom ⊢ φ → supp Z⁡ F ∪ supp Z⁡ G ∈ Fin