Metamath Proof Explorer

Theorem ressuppfi

Description: If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019)

Ref Expression
Hypotheses ressuppfi.b ⊢ φ → dom ⁡ F ∖ B ∈ Fin
ressuppfi.f ⊢ φ → F ∈ W
ressuppfi.g ⊢ φ → G = F ↾ B
ressuppfi.s ⊢ φ → G supp Z ∈ Fin
ressuppfi.z ⊢ φ → Z ∈ V
Assertion ressuppfi ⊢ φ → F supp Z ∈ Fin

Proof

Step Hyp Ref Expression
1 ressuppfi.b ⊢ φ → dom ⁡ F ∖ B ∈ Fin
2 ressuppfi.f ⊢ φ → F ∈ W
3 ressuppfi.g ⊢ φ → G = F ↾ B
4 ressuppfi.s ⊢ φ → G supp Z ∈ Fin
5 ressuppfi.z ⊢ φ → Z ∈ V
6 3 eqcomd ⊢ φ → F ↾ B = G
7 6 oveq1d ⊢ φ → F ↾ B supp Z = G supp Z
8 7 4 eqeltrd ⊢ φ → F ↾ B supp Z ∈ Fin
9 unfi ⊢ F ↾ B supp Z ∈ Fin ∧ dom ⁡ F ∖ B ∈ Fin → supp Z⁡ F ↾ B ∪ dom ⁡ F ∖ B ∈ Fin
10 8 1 9 syl2anc ⊢ φ → supp Z⁡ F ↾ B ∪ dom ⁡ F ∖ B ∈ Fin
11 ressuppssdif ⊢ F ∈ W ∧ Z ∈ V → F supp Z ⊆ supp Z⁡ F ↾ B ∪ dom ⁡ F ∖ B
12 2 5 11 syl2anc ⊢ φ → F supp Z ⊆ supp Z⁡ F ↾ B ∪ dom ⁡ F ∖ B
13 10 12 ssfid ⊢ φ → F supp Z ∈ Fin