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 𝑍 )