This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resfsupp

Description: If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019)

Ref Expression
Hypotheses resfsupp.b ⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
resfsupp.e ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
resfsupp.f ⊢ ( 𝜑 → Fun 𝐹 )
resfsupp.g ⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
resfsupp.s ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
resfsupp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion resfsupp ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 resfsupp.b ⊢ ( 𝜑 → ( dom 𝐹 ∖ 𝐵 ) ∈ Fin )
2 resfsupp.e ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
3 resfsupp.f ⊢ ( 𝜑 → Fun 𝐹 )
4 resfsupp.g ⊢ ( 𝜑 → 𝐺 = ( 𝐹 ↾ 𝐵 ) )
5 resfsupp.s ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
6 resfsupp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
7 5 fsuppimpd ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
8 1 2 4 7 6 ressuppfi ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
9 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
10 3 2 6 9 syl3anc ⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
11 8 10 mpbird ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )