Metamath Proof Explorer

Theorem fsuppun

Description: The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019)

Ref Expression
Hypotheses fsuppun.f ⊢ φ → finSupp Z⁡ F
fsuppun.g ⊢ φ → finSupp Z⁡ G
Assertion fsuppun ⊢ φ → F ∪ G supp Z ∈ Fin

Proof

Step Hyp Ref Expression
1 fsuppun.f ⊢ φ → finSupp Z⁡ F
2 fsuppun.g ⊢ φ → finSupp Z⁡ G
3 cnvun ⊢ F ∪ G -1 = F -1 ∪ G -1
4 3 imaeq1i ⊢ F ∪ G -1 V ∖ Z = F -1 ∪ G -1 V ∖ Z
5 imaundir ⊢ F -1 ∪ G -1 V ∖ Z = F -1 V ∖ Z ∪ G -1 V ∖ Z
6 4 5 eqtri ⊢ F ∪ G -1 V ∖ Z = F -1 V ∖ Z ∪ G -1 V ∖ Z
7 unexb ⊢ F ∈ V ∧ G ∈ V ↔ F ∪ G ∈ V
8 simpl ⊢ F ∈ V ∧ G ∈ V → F ∈ V
9 7 8 sylbir ⊢ F ∪ G ∈ V → F ∈ V
10 suppimacnv ⊢ F ∈ V ∧ Z ∈ V → F supp Z = F -1 V ∖ Z
11 9 10 sylan ⊢ F ∪ G ∈ V ∧ Z ∈ V → F supp Z = F -1 V ∖ Z
12 11 eqcomd ⊢ F ∪ G ∈ V ∧ Z ∈ V → F -1 V ∖ Z = F supp Z
13 12 adantr ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F -1 V ∖ Z = F supp Z
14 1 fsuppimpd ⊢ φ → F supp Z ∈ Fin
15 14 adantl ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F supp Z ∈ Fin
16 13 15 eqeltrd ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F -1 V ∖ Z ∈ Fin
17 simpr ⊢ F ∈ V ∧ G ∈ V → G ∈ V
18 7 17 sylbir ⊢ F ∪ G ∈ V → G ∈ V
19 suppimacnv ⊢ G ∈ V ∧ Z ∈ V → G supp Z = G -1 V ∖ Z
20 19 eqcomd ⊢ G ∈ V ∧ Z ∈ V → G -1 V ∖ Z = G supp Z
21 18 20 sylan ⊢ F ∪ G ∈ V ∧ Z ∈ V → G -1 V ∖ Z = G supp Z
22 21 adantr ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → G -1 V ∖ Z = G supp Z
23 2 fsuppimpd ⊢ φ → G supp Z ∈ Fin
24 23 adantl ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → G supp Z ∈ Fin
25 22 24 eqeltrd ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → G -1 V ∖ Z ∈ Fin
26 unfi ⊢ F -1 V ∖ Z ∈ Fin ∧ G -1 V ∖ Z ∈ Fin → F -1 V ∖ Z ∪ G -1 V ∖ Z ∈ Fin
27 16 25 26 syl2anc ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F -1 V ∖ Z ∪ G -1 V ∖ Z ∈ Fin
28 6 27 eqeltrid ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F ∪ G -1 V ∖ Z ∈ Fin
29 suppimacnv ⊢ F ∪ G ∈ V ∧ Z ∈ V → F ∪ G supp Z = F ∪ G -1 V ∖ Z
30 29 eleq1d ⊢ F ∪ G ∈ V ∧ Z ∈ V → F ∪ G supp Z ∈ Fin ↔ F ∪ G -1 V ∖ Z ∈ Fin
31 30 adantr ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F ∪ G supp Z ∈ Fin ↔ F ∪ G -1 V ∖ Z ∈ Fin
32 28 31 mpbird ⊢ F ∪ G ∈ V ∧ Z ∈ V ∧ φ → F ∪ G supp Z ∈ Fin
33 32 ex ⊢ F ∪ G ∈ V ∧ Z ∈ V → φ → F ∪ G supp Z ∈ Fin
34 supp0prc ⊢ ¬ F ∪ G ∈ V ∧ Z ∈ V → F ∪ G supp Z = ∅
35 0fin ⊢ ∅ ∈ Fin
36 34 35 eqeltrdi ⊢ ¬ F ∪ G ∈ V ∧ Z ∈ V → F ∪ G supp Z ∈ Fin
37 36 a1d ⊢ ¬ F ∪ G ∈ V ∧ Z ∈ V → φ → F ∪ G supp Z ∈ Fin
38 33 37 pm2.61i ⊢ φ → F ∪ G supp Z ∈ Fin