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